Metamath Proof Explorer

Theorem un01

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

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

Proof

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