Theorem in1 42191

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

Syntax hints:   → wi 4  (   wvd1 42189

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 42190

This theorem is referenced by:  vd12  42220  vd13  42221  gen11nv  42237  gen12  42238  exinst11  42246  e1a  42247  el1  42248  e223  42255  e111  42294  e1111  42295  el2122old  42339  el12  42346  el123  42384  un0.1  42399  trsspwALT  42438  sspwtr  42441  pwtrVD  42444  pwtrrVD  42445  snssiALTVD  42447  snsslVD  42449  snelpwrVD  42451  unipwrVD  42452  sstrALT2VD  42454  suctrALT2VD  42456  elex2VD  42458  elex22VD  42459  eqsbc2VD  42460  zfregs2VD  42461  tpid3gVD  42462  en3lplem1VD  42463  en3lplem2VD  42464  en3lpVD  42465  3ornot23VD  42467  orbi1rVD  42468  3orbi123VD  42470  sbc3orgVD  42471  19.21a3con13vVD  42472  exbirVD  42473  exbiriVD  42474  rspsbc2VD  42475  3impexpVD  42476  3impexpbicomVD  42477  sbcoreleleqVD  42479  tratrbVD  42481  al2imVD  42482  syl5impVD  42483  ssralv2VD  42486  ordelordALTVD  42487  equncomVD  42488  imbi12VD  42493  imbi13VD  42494  sbcim2gVD  42495  sbcbiVD  42496  trsbcVD  42497  truniALTVD  42498  trintALTVD  42500  undif3VD  42502  sbcssgVD  42503  csbingVD  42504  simplbi2comtVD  42508  onfrALTVD  42511  csbeq2gVD  42512  csbsngVD  42513  csbxpgVD  42514  csbresgVD  42515  csbrngVD  42516  csbima12gALTVD  42517  csbunigVD  42518  csbfv12gALTVD  42519  con5VD  42520  relopabVD  42521  19.41rgVD  42522  2pm13.193VD  42523  hbimpgVD  42524  hbalgVD  42525  hbexgVD  42526  ax6e2eqVD  42527  ax6e2ndVD  42528  ax6e2ndeqVD  42529  2sb5ndVD  42530  2uasbanhVD  42531  e2ebindVD  42532  sb5ALTVD  42533  vk15.4jVD  42534  notnotrALTVD  42535  con3ALTVD  42536  sspwimpVD  42539  sspwimpcfVD  42541  suctrALTcfVD  42543