Theorem dfvd1ir 44665

Description: Inference form of df-vd1 44662 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	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
dfvd1ir	⊢ (   𝜑   ▶   𝜓   )

Proof of Theorem dfvd1ir

Step	Hyp	Ref	Expression
1		dfvd1ir.1	. 2 ⊢ (𝜑 → 𝜓)
2		df-vd1 44662	. 2 ⊢ ((   𝜑   ▶   𝜓   ) ↔ (𝜑 → 𝜓))
3	1, 2	mpbir 231	1 ⊢ (   𝜑   ▶   𝜓   )

Syntax hints:   → wi 4  (   wvd1 44661

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 207  df-vd1 44662

This theorem is referenced by:  idn1  44666  vd01  44689  in2  44697  int2  44698  gen11nv  44709  gen12  44710  exinst01  44717  exinst11  44718  e1a  44719  el1  44720  e111  44766  e1111  44767  un0.1  44870  un10  44879  un01  44880  sbcoreleleqVD  44950  2uasbanhVD  45002