Theorem dfvd1ir 39555

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

Syntax hints:   → wi 4  (   wvd1 39551

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 199  df-vd1 39552

This theorem is referenced by:  idn1  39556  vd01  39588  in2  39596  int2  39597  gen11nv  39608  gen12  39609  exinst01  39616  exinst11  39617  e1a  39618  el1  39619  e111  39665  e1111  39666  un0.1  39771  un10  39780  un01  39781  sbcoreleleqVD  39851  2uasbanhVD  39903