Metamath Proof Explorer

Theorem uunT11p1

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

Proof

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