Theorem dfvd1ir 41279

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

Syntax hints:   → wi 4  (   wvd1 41275

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 41276

This theorem is referenced by:  idn1  41280  vd01  41303  in2  41311  int2  41312  gen11nv  41323  gen12  41324  exinst01  41331  exinst11  41332  e1a  41333  el1  41334  e111  41380  e1111  41381  un0.1  41485  un10  41494  un01  41495  sbcoreleleqVD  41565  2uasbanhVD  41617