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 φ ψ