Theorem dfvd1ir 39106

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

Syntax hints:   → wi 4  (   wvd1 39102

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 197  df-vd1 39103

This theorem is referenced by:  idn1  39107  vd01  39139  in2  39147  int2  39148  gen11nv  39159  gen12  39160  exinst01  39167  exinst11  39168  e1a  39169  el1  39170  e111  39216  e1111  39217  un0.1  39323  un10  39332  un01  39333  2uasbanhVD  39461