Theorem dfvd1ir 45494

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

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

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 45491

This theorem is used by:  idn1  45495  vd01  45518  in2  45526  int2  45527  gen11nv  45538  gen12  45539  exinst01  45546  exinst11  45547  e1a  45548  el1  45549  e111  45595  e1111  45596  un0.1  45699  un10  45708  un01  45709  sbcoreleleqVD  45779  2uasbanhVD  45831