Theorem in1 45144

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

Syntax hints:   → wi 4  (   wvd1 45142

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 209  df-vd1 45143

This theorem is referenced by:  vd12  45173  vd13  45174  gen11nv  45190  gen12  45191  exinst11  45199  e1a  45200  el1  45201  e223  45208  e111  45247  e1111  45248  el2122old  45291  el12  45298  el123  45336  un0.1  45351  trsspwALT  45390  sspwtr  45393  pwtrVD  45396  pwtrrVD  45397  snssiALTVD  45399  snsslVD  45401  snelpwrVD  45403  unipwrVD  45404  sstrALT2VD  45406  suctrALT2VD  45408  elex2VD  45410  elex22VD  45411  eqsbc2VD  45412  zfregs2VD  45413  tpid3gVD  45414  en3lplem1VD  45415  en3lplem2VD  45416  en3lpVD  45417  3ornot23VD  45419  orbi1rVD  45420  3orbi123VD  45422  sbc3orgVD  45423  19.21a3con13vVD  45424  exbirVD  45425  exbiriVD  45426  rspsbc2VD  45427  3impexpVD  45428  3impexpbicomVD  45429  sbcoreleleqVD  45431  tratrbVD  45433  al2imVD  45434  syl5impVD  45435  ssralv2VD  45438  ordelordALTVD  45439  equncomVD  45440  imbi12VD  45445  imbi13VD  45446  sbcim2gVD  45447  sbcbiVD  45448  trsbcVD  45449  truniALTVD  45450  trintALTVD  45452  undif3VD  45454  sbcssgVD  45455  csbingVD  45456  simplbi2comtVD  45460  onfrALTVD  45463  csbeq2gVD  45464  csbsngVD  45465  csbxpgVD  45466  csbresgVD  45467  csbrngVD  45468  csbima12gALTVD  45469  csbunigVD  45470  csbfv12gALTVD  45471  con5VD  45472  relopabVD  45473  19.41rgVD  45474  2pm13.193VD  45475  hbimpgVD  45476  hbalgVD  45477  hbexgVD  45478  ax6e2eqVD  45479  ax6e2ndVD  45480  ax6e2ndeqVD  45481  2sb5ndVD  45482  2uasbanhVD  45483  e2ebindVD  45484  sb5ALTVD  45485  vk15.4jVD  45486  notnotrALTVD  45487  con3ALTVD  45488  sspwimpVD  45491  sspwimpcfVD  45493  suctrALTcfVD  45495