Theorem dfvd1ir 45154

Description: Inference form of df-vd1 45151 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 45151	. 2 ⊢ ((   𝜑   ▶   𝜓   ) ↔ (𝜑 → 𝜓))
3	1, 2	mpbir 233	1 ⊢ (   𝜑   ▶   𝜓   )

Syntax hints:   → wi 4  (   wvd1 45150

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 209  df-vd1 45151

This theorem is referenced by:  idn1  45155  vd01  45178  in2  45186  int2  45187  gen11nv  45198  gen12  45199  exinst01  45206  exinst11  45207  e1a  45208  el1  45209  e111  45255  e1111  45256  un0.1  45359  un10  45368  un01  45369  sbcoreleleqVD  45439  2uasbanhVD  45491