Theorem dfvd1ir 45230

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

Syntax hints:   → wi 4  (   wvd1 45226

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 45227

This theorem is referenced by:  idn1  45231  vd01  45254  in2  45262  int2  45263  gen11nv  45274  gen12  45275  exinst01  45282  exinst11  45283  e1a  45284  el1  45285  e111  45331  e1111  45332  un0.1  45435  un10  45444  un01  45445  sbcoreleleqVD  45515  2uasbanhVD  45567