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

Metamath Proof Explorer

Theorem uun2221p2

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

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

Proof

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