Metamath Proof Explorer

Theorem uunT11p2

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

Proof

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