Metamath Proof Explorer

Theorem un10

Description: A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis un10.1 
|- (. (. ph ,. T. ). ->. ps ).
Assertion un10 
|- (. ph ->. ps ).

Proof

Step Hyp Ref Expression
1 un10.1 
 |-  (. (. ph ,. T. ). ->. ps ).
2 tru 
 |-  T.
3 2 jctr 
 |-  ( ph -> ( ph /\ T. ) )
4 1 dfvd2ani 
 |-  ( ( ph /\ T. ) -> ps )
5 3 4 syl 
 |-  ( ph -> ps )
6 5 dfvd1ir 
 |-  (. ph ->. ps ).