Theorem dfvd1ir 44997

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

Syntax hints:   → wi 4  (   wvd1 44993

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 44994

This theorem is referenced by:  idn1  44998  vd01  45021  in2  45029  int2  45030  gen11nv  45041  gen12  45042  exinst01  45049  exinst11  45050  e1a  45051  el1  45052  e111  45098  e1111  45099  un0.1  45202  un10  45211  un01  45212  sbcoreleleqVD  45282  2uasbanhVD  45334