This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uun2221

Description: A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 30-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis uun2221.1 ⊢ ( ( 𝜑 ∧ 𝜑 ∧ ( 𝜓 ∧ 𝜑 ) ) → 𝜒 )
Assertion uun2221 ( ( 𝜓 ∧ 𝜑 ) → 𝜒 )

Proof

Step Hyp Ref Expression
1 uun2221.1 ⊢ ( ( 𝜑 ∧ 𝜑 ∧ ( 𝜓 ∧ 𝜑 ) ) → 𝜒 )
2 3anass ⊢ ( ( 𝜑 ∧ 𝜑 ∧ ( 𝜓 ∧ 𝜑 ) ) ↔ ( 𝜑 ∧ ( 𝜑 ∧ ( 𝜓 ∧ 𝜑 ) ) ) )
3 anabs5 ⊢ ( ( 𝜑 ∧ ( 𝜑 ∧ ( 𝜓 ∧ 𝜑 ) ) ) ↔ ( 𝜑 ∧ ( 𝜓 ∧ 𝜑 ) ) )
4 2 3 bitri ⊢ ( ( 𝜑 ∧ 𝜑 ∧ ( 𝜓 ∧ 𝜑 ) ) ↔ ( 𝜑 ∧ ( 𝜓 ∧ 𝜑 ) ) )
5 ancom ⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜓 ∧ 𝜑 ) )
6 5 anbi2i ⊢ ( ( 𝜑 ∧ ( 𝜑 ∧ 𝜓 ) ) ↔ ( 𝜑 ∧ ( 𝜓 ∧ 𝜑 ) ) )
7 4 6 bitr4i ⊢ ( ( 𝜑 ∧ 𝜑 ∧ ( 𝜓 ∧ 𝜑 ) ) ↔ ( 𝜑 ∧ ( 𝜑 ∧ 𝜓 ) ) )
8 anabs5 ⊢ ( ( 𝜑 ∧ ( 𝜑 ∧ 𝜓 ) ) ↔ ( 𝜑 ∧ 𝜓 ) )
9 8 5 bitri ⊢ ( ( 𝜑 ∧ ( 𝜑 ∧ 𝜓 ) ) ↔ ( 𝜓 ∧ 𝜑 ) )
10 7 9 bitri ⊢ ( ( 𝜑 ∧ 𝜑 ∧ ( 𝜓 ∧ 𝜑 ) ) ↔ ( 𝜓 ∧ 𝜑 ) )
11 10 imbi1i ⊢ ( ( ( 𝜑 ∧ 𝜑 ∧ ( 𝜓 ∧ 𝜑 ) ) → 𝜒 ) ↔ ( ( 𝜓 ∧ 𝜑 ) → 𝜒 ) )
12 1 11 mpbi ⊢ ( ( 𝜓 ∧ 𝜑 ) → 𝜒 )