Theorem in1 43846

Description: Inference form of df-vd1 43845. Virtual deduction introduction rule of converting the virtual hypothesis of a 1-virtual hypothesis virtual deduction into an antecedent. (Contributed by Alan Sare, 14-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
in1.1	⊢ (   𝜑   ▶   𝜓   )

Assertion

Ref	Expression
in1	⊢ (𝜑 → 𝜓)

Proof of Theorem in1

Step	Hyp	Ref	Expression
1		in1.1	. 2 ⊢ (   𝜑   ▶   𝜓   )
2		df-vd1 43845	. 2 ⊢ ((   𝜑   ▶   𝜓   ) ↔ (𝜑 → 𝜓))
3	1, 2	mpbi 229	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4  (   wvd1 43844

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 206  df-vd1 43845

This theorem is referenced by:  vd12  43875  vd13  43876  gen11nv  43892  gen12  43893  exinst11  43901  e1a  43902  el1  43903  e223  43910  e111  43949  e1111  43950  el2122old  43994  el12  44001  el123  44039  un0.1  44054  trsspwALT  44093  sspwtr  44096  pwtrVD  44099  pwtrrVD  44100  snssiALTVD  44102  snsslVD  44104  snelpwrVD  44106  unipwrVD  44107  sstrALT2VD  44109  suctrALT2VD  44111  elex2VD  44113  elex22VD  44114  eqsbc2VD  44115  zfregs2VD  44116  tpid3gVD  44117  en3lplem1VD  44118  en3lplem2VD  44119  en3lpVD  44120  3ornot23VD  44122  orbi1rVD  44123  3orbi123VD  44125  sbc3orgVD  44126  19.21a3con13vVD  44127  exbirVD  44128  exbiriVD  44129  rspsbc2VD  44130  3impexpVD  44131  3impexpbicomVD  44132  sbcoreleleqVD  44134  tratrbVD  44136  al2imVD  44137  syl5impVD  44138  ssralv2VD  44141  ordelordALTVD  44142  equncomVD  44143  imbi12VD  44148  imbi13VD  44149  sbcim2gVD  44150  sbcbiVD  44151  trsbcVD  44152  truniALTVD  44153  trintALTVD  44155  undif3VD  44157  sbcssgVD  44158  csbingVD  44159  simplbi2comtVD  44163  onfrALTVD  44166  csbeq2gVD  44167  csbsngVD  44168  csbxpgVD  44169  csbresgVD  44170  csbrngVD  44171  csbima12gALTVD  44172  csbunigVD  44173  csbfv12gALTVD  44174  con5VD  44175  relopabVD  44176  19.41rgVD  44177  2pm13.193VD  44178  hbimpgVD  44179  hbalgVD  44180  hbexgVD  44181  ax6e2eqVD  44182  ax6e2ndVD  44183  ax6e2ndeqVD  44184  2sb5ndVD  44185  2uasbanhVD  44186  e2ebindVD  44187  sb5ALTVD  44188  vk15.4jVD  44189  notnotrALTVD  44190  con3ALTVD  44191  sspwimpVD  44194  sspwimpcfVD  44196  suctrALTcfVD  44198