Theorem dfvd1ir 38789

Description: Inference form of df-vd1 38786 with the virtual deduction as the assertion. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
dfvd1ir.1	|- ( ph -> ps )

Assertion

Ref	Expression
dfvd1ir	|- (. ph ->. ps ).

Proof of Theorem dfvd1ir

Step	Hyp	Ref	Expression
1		dfvd1ir.1	. 2 |- ( ph -> ps )
2		df-vd1 38786	. 2 |- ( (. ph ->. ps ). <-> ( ph -> ps ) )
3	1, 2	mpbir 221	1 |- (. ph ->. ps ).

Syntax hints:   -> wi 4   (.wvd1 38785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-vd1 38786

This theorem is referenced by:  idn1  38790  vd01  38822  in2  38830  int2  38831  gen11nv  38842  gen12  38843  exinst01  38850  exinst11  38851  e1a  38852  el1  38853  e111  38899  e1111  38900  un0.1  39006  un10  39015  un01  39016  2uasbanhVD  39147