Theorem dfvd1ir 43324

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

Syntax hints:   → wi 4  (   wvd1 43320

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 206  df-vd1 43321

This theorem is referenced by:  idn1  43325  vd01  43348  in2  43356  int2  43357  gen11nv  43368  gen12  43369  exinst01  43376  exinst11  43377  e1a  43378  el1  43379  e111  43425  e1111  43426  un0.1  43530  un10  43539  un01  43540  sbcoreleleqVD  43610  2uasbanhVD  43662