Theorem dfvd1ir 37604

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

Syntax hints:   → wi 4  (   wvd1 37600

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 196  df-vd1 37601

This theorem is referenced by:  idn1  37605  vd01  37637  in2  37645  int2  37646  gen11nv  37657  gen12  37658  exinst01  37665  exinst11  37666  e1a  37667  el1  37668  e111  37714  e1111  37715  un0.1  37821  un10  37830  un01  37831  2uasbanhVD  37963