Theorem dfvd1ir 45383

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

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

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 45380

This theorem is used by:  idn1  45384  vd01  45407  in2  45415  int2  45416  gen11nv  45427  gen12  45428  exinst01  45435  exinst11  45436  e1a  45437  el1  45438  e111  45484  e1111  45485  un0.1  45588  un10  45597  un01  45598  sbcoreleleqVD  45668  2uasbanhVD  45720