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