Theorem dfvd1ir 44563

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

Syntax hints:   → wi 4  (   wvd1 44559

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 44560

This theorem is referenced by:  idn1  44564  vd01  44587  in2  44595  int2  44596  gen11nv  44607  gen12  44608  exinst01  44615  exinst11  44616  e1a  44617  el1  44618  e111  44664  e1111  44665  un0.1  44768  un10  44777  un01  44778  sbcoreleleqVD  44848  2uasbanhVD  44900