Metamath Proof Explorer

Theorem uunTT1p2

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

Proof

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