Metamath Proof Explorer

Definition df-vd1

Description: Definition of virtual deduction. (Contributed by Alan Sare, 21-Apr-2011) (New usage is discouraged.)

Ref Expression
Assertion df-vd1 
|- ( (. ph ->. ps ). <-> ( ph -> ps ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph 
 |-  ph
1 wps 
 |-  ps
2 0 1 wvd1 
 |-  (. ph ->. ps ).
3 0 1 wi 
 |-  ( ph -> ps )
4 2 3 wb 
 |-  ( (. ph ->. ps ). <-> ( ph -> ps ) )