Theorem dfvd1ir 45745

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

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

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 45742

This theorem is used by:  idn1  45746  vd01  45769  in2  45777  int2  45778  gen11nv  45789  gen12  45790  exinst01  45797  exinst11  45798  e1a  45799  el1  45800  e111  45846  e1111  45847  un0.1  45950  un10  45959  un01  45960  sbcoreleleqVD  46030  2uasbanhVD  46082