Theorem in1 45171

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

Syntax hints:   → wi 4  (   wvd1 45169

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 210  df-vd1 45170

This theorem is referenced by:  vd12  45200  vd13  45201  gen11nv  45217  gen12  45218  exinst11  45226  e1a  45227  el1  45228  e223  45235  e111  45274  e1111  45275  el2122old  45318  el12  45325  el123  45363  un0.1  45378  trsspwALT  45417  sspwtr  45420  pwtrVD  45423  pwtrrVD  45424  snssiALTVD  45426  snsslVD  45428  snelpwrVD  45430  unipwrVD  45431  sstrALT2VD  45433  suctrALT2VD  45435  elex2VD  45437  elex22VD  45438  eqsbc2VD  45439  zfregs2VD  45440  tpid3gVD  45441  en3lplem1VD  45442  en3lplem2VD  45443  en3lpVD  45444  3ornot23VD  45446  orbi1rVD  45447  3orbi123VD  45449  sbc3orgVD  45450  19.21a3con13vVD  45451  exbirVD  45452  exbiriVD  45453  rspsbc2VD  45454  3impexpVD  45455  3impexpbicomVD  45456  sbcoreleleqVD  45458  tratrbVD  45460  al2imVD  45461  syl5impVD  45462  ssralv2VD  45465  ordelordALTVD  45466  equncomVD  45467  imbi12VD  45472  imbi13VD  45473  sbcim2gVD  45474  sbcbiVD  45475  trsbcVD  45476  truniALTVD  45477  trintALTVD  45479  undif3VD  45481  sbcssgVD  45482  csbingVD  45483  simplbi2comtVD  45487  onfrALTVD  45490  csbeq2gVD  45491  csbsngVD  45492  csbxpgVD  45493  csbresgVD  45494  csbrngVD  45495  csbima12gALTVD  45496  csbunigVD  45497  csbfv12gALTVD  45498  con5VD  45499  relopabVD  45500  19.41rgVD  45501  2pm13.193VD  45502  hbimpgVD  45503  hbalgVD  45504  hbexgVD  45505  ax6e2eqVD  45506  ax6e2ndVD  45507  ax6e2ndeqVD  45508  2sb5ndVD  45509  2uasbanhVD  45510  e2ebindVD  45511  sb5ALTVD  45512  vk15.4jVD  45513  notnotrALTVD  45514  con3ALTVD  45515  sspwimpVD  45518  sspwimpcfVD  45520  suctrALTcfVD  45522