Theorem dfvd1ir 44556

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

Syntax hints:   → wi 4  (   wvd1 44552

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 44553

This theorem is referenced by:  idn1  44557  vd01  44580  in2  44588  int2  44589  gen11nv  44600  gen12  44601  exinst01  44608  exinst11  44609  e1a  44610  el1  44611  e111  44657  e1111  44658  un0.1  44761  un10  44770  un01  44771  sbcoreleleqVD  44841  2uasbanhVD  44893