Theorem dfvd1ir 43382

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

Syntax hints:   → wi 4  (   wvd1 43378

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 43379

This theorem is referenced by:  idn1  43383  vd01  43406  in2  43414  int2  43415  gen11nv  43426  gen12  43427  exinst01  43434  exinst11  43435  e1a  43436  el1  43437  e111  43483  e1111  43484  un0.1  43588  un10  43597  un01  43598  sbcoreleleqVD  43668  2uasbanhVD  43720