Theorem dfvd1ir 45003

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

Syntax hints:   → wi 4  (   wvd1 44999

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 45000

This theorem is referenced by:  idn1  45004  vd01  45027  in2  45035  int2  45036  gen11nv  45047  gen12  45048  exinst01  45055  exinst11  45056  e1a  45057  el1  45058  e111  45104  e1111  45105  un0.1  45208  un10  45217  un01  45218  sbcoreleleqVD  45288  2uasbanhVD  45340