Theorem dfvd1ir 44593

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

Syntax hints:   → wi 4  (   wvd1 44589

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 44590

This theorem is referenced by:  idn1  44594  vd01  44617  in2  44625  int2  44626  gen11nv  44637  gen12  44638  exinst01  44645  exinst11  44646  e1a  44647  el1  44648  e111  44694  e1111  44695  un0.1  44799  un10  44808  un01  44809  sbcoreleleqVD  44879  2uasbanhVD  44931