Theorem dfvd1ir 44536

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

Syntax hints:   → wi 4  (   wvd1 44532

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 44533

This theorem is referenced by:  idn1  44537  vd01  44560  in2  44568  int2  44569  gen11nv  44580  gen12  44581  exinst01  44588  exinst11  44589  e1a  44590  el1  44591  e111  44637  e1111  44638  un0.1  44741  un10  44750  un01  44751  sbcoreleleqVD  44821  2uasbanhVD  44873