Theorem dfvd1ir 45556

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

This proof depends on syntax axioms:   → wi 4  (   wvd1 45552

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-vd1 45553

This theorem is used by:  idn1  45557  vd01  45580  in2  45588  int2  45589  gen11nv  45600  gen12  45601  exinst01  45608  exinst11  45609  e1a  45610  el1  45611  e111  45657  e1111  45658  un0.1  45761  un10  45770  un01  45771  sbcoreleleqVD  45841  2uasbanhVD  45893