Theorem dfvd1ir 45169

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

Syntax hints:   → wi 4  (   wvd1 45165

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 210  df-vd1 45166

This theorem is referenced by:  idn1  45170  vd01  45193  in2  45201  int2  45202  gen11nv  45213  gen12  45214  exinst01  45221  exinst11  45222  e1a  45223  el1  45224  e111  45270  e1111  45271  un0.1  45374  un10  45383  un01  45384  sbcoreleleqVD  45454  2uasbanhVD  45506