Metamath Proof Explorer

Theorem uunT12p4

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

Proof

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