Theorem in1 39104

Description: Inference form of df-vd1 39103. 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 39103	. 2 ⊢ ((   𝜑   ▶   𝜓   ) ↔ (𝜑 → 𝜓))
3	1, 2	mpbi 220	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:  vd12  39142  vd13  39143  gen11nv  39159  gen12  39160  exinst11  39168  e1a  39169  el1  39170  e223  39177  e111  39216  e1111  39217  el2122old  39261  el12  39270  el123  39308  un0.1  39323  trsspwALT  39362  sspwtr  39365  pwtrVD  39373  pwtrrVD  39374  snssiALTVD  39376  snsslVD  39378  snelpwrVD  39380  unipwrVD  39381  sstrALT2VD  39383  suctrALT2VD  39385  elex2VD  39387  elex22VD  39388  eqsbc3rVD  39389  zfregs2VD  39390  tpid3gVD  39391  en3lplem1VD  39392  en3lplem2VD  39393  en3lpVD  39394  3ornot23VD  39396  orbi1rVD  39397  3orbi123VD  39399  sbc3orgVD  39400  19.21a3con13vVD  39401  exbirVD  39402  exbiriVD  39403  rspsbc2VD  39404  3impexpVD  39405  3impexpbicomVD  39406  sbcoreleleqVD  39409  tratrbVD  39411  al2imVD  39412  syl5impVD  39413  ssralv2VD  39416  ordelordALTVD  39417  equncomVD  39418  imbi12VD  39423  imbi13VD  39424  sbcim2gVD  39425  sbcbiVD  39426  trsbcVD  39427  truniALTVD  39428  trintALTVD  39430  undif3VD  39432  sbcssgVD  39433  csbingVD  39434  simplbi2comtVD  39438  onfrALTVD  39441  csbeq2gVD  39442  csbsngVD  39443  csbxpgVD  39444  csbresgVD  39445  csbrngVD  39446  csbima12gALTVD  39447  csbunigVD  39448  csbfv12gALTVD  39449  con5VD  39450  relopabVD  39451  19.41rgVD  39452  2pm13.193VD  39453  hbimpgVD  39454  hbalgVD  39455  hbexgVD  39456  ax6e2eqVD  39457  ax6e2ndVD  39458  ax6e2ndeqVD  39459  2sb5ndVD  39460  2uasbanhVD  39461  e2ebindVD  39462  sb5ALTVD  39463  vk15.4jVD  39464  notnotrALTVD  39465  con3ALTVD  39466  sspwimpVD  39469  sspwimpcfVD  39471  suctrALTcfVD  39473