Metamath Proof Explorer


Theorem uunTT1p2

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

Proof

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