Theorem dfvd1ir 45310

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

This proof depends on syntax axioms:   → wi 4  (   wvd1 45306

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-vd1 45307

This theorem is used by:  idn1  45311  vd01  45334  in2  45342  int2  45343  gen11nv  45354  gen12  45355  exinst01  45362  exinst11  45363  e1a  45364  el1  45365  e111  45411  e1111  45412  un0.1  45515  un10  45524  un01  45525  sbcoreleleqVD  45595  2uasbanhVD  45647