Metamath Proof Explorer

Theorem uunT12p1

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 uunT12p1.1 ⊢ ⊤ ∧ ψ ∧ φ → χ
Assertion uunT12p1 ⊢ φ ∧ ψ → χ

Proof

Step Hyp Ref Expression
1 uunT12p1.1 ⊢ ⊤ ∧ ψ ∧ φ → χ
2 3anass ⊢ ⊤ ∧ ψ ∧ φ ↔ ⊤ ∧ ψ ∧ φ
3 truan ⊢ ⊤ ∧ ψ ∧ φ ↔ ψ ∧ φ
4 2 3 bitri ⊢ ⊤ ∧ ψ ∧ φ ↔ ψ ∧ φ
5 ancom ⊢ φ ∧ ψ ↔ ψ ∧ φ
6 4 5 bitr4i ⊢ ⊤ ∧ ψ ∧ φ ↔ φ ∧ ψ
7 6 1 sylbir ⊢ φ ∧ ψ → χ