Metamath Proof Explorer


Theorem uunT12p2

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 uunT12p2.1
|- ( ( ph /\ T. /\ ps ) -> ch )
Assertion uunT12p2
|- ( ( ph /\ ps ) -> ch )

Proof

Step Hyp Ref Expression
1 uunT12p2.1
 |-  ( ( ph /\ T. /\ ps ) -> ch )
2 3anrot
 |-  ( ( ph /\ T. /\ ps ) <-> ( T. /\ ps /\ ph ) )
3 3anass
 |-  ( ( T. /\ ps /\ ph ) <-> ( T. /\ ( ps /\ ph ) ) )
4 2 3 bitri
 |-  ( ( ph /\ T. /\ ps ) <-> ( T. /\ ( ps /\ ph ) ) )
5 truan
 |-  ( ( T. /\ ( ps /\ ph ) ) <-> ( ps /\ ph ) )
6 4 5 bitri
 |-  ( ( ph /\ T. /\ ps ) <-> ( ps /\ ph ) )
7 ancom
 |-  ( ( ph /\ ps ) <-> ( ps /\ ph ) )
8 6 7 bitr4i
 |-  ( ( ph /\ T. /\ ps ) <-> ( ph /\ ps ) )
9 8 1 sylbir
 |-  ( ( ph /\ ps ) -> ch )