Theorem dfvd1ir 44892

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

Syntax hints:   → wi 4  (   wvd1 44888

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 207  df-vd1 44889

This theorem is referenced by:  idn1  44893  vd01  44916  in2  44924  int2  44925  gen11nv  44936  gen12  44937  exinst01  44944  exinst11  44945  e1a  44946  el1  44947  e111  44993  e1111  44994  un0.1  45097  un10  45106  un01  45107  sbcoreleleqVD  45177  2uasbanhVD  45229