Theorem in1 42080

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

Syntax hints:   → wi 4  (   wvd1 42078

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 42079

This theorem is referenced by:  vd12  42109  vd13  42110  gen11nv  42126  gen12  42127  exinst11  42135  e1a  42136  el1  42137  e223  42144  e111  42183  e1111  42184  el2122old  42228  el12  42235  el123  42273  un0.1  42288  trsspwALT  42327  sspwtr  42330  pwtrVD  42333  pwtrrVD  42334  snssiALTVD  42336  snsslVD  42338  snelpwrVD  42340  unipwrVD  42341  sstrALT2VD  42343  suctrALT2VD  42345  elex2VD  42347  elex22VD  42348  eqsbc2VD  42349  zfregs2VD  42350  tpid3gVD  42351  en3lplem1VD  42352  en3lplem2VD  42353  en3lpVD  42354  3ornot23VD  42356  orbi1rVD  42357  3orbi123VD  42359  sbc3orgVD  42360  19.21a3con13vVD  42361  exbirVD  42362  exbiriVD  42363  rspsbc2VD  42364  3impexpVD  42365  3impexpbicomVD  42366  sbcoreleleqVD  42368  tratrbVD  42370  al2imVD  42371  syl5impVD  42372  ssralv2VD  42375  ordelordALTVD  42376  equncomVD  42377  imbi12VD  42382  imbi13VD  42383  sbcim2gVD  42384  sbcbiVD  42385  trsbcVD  42386  truniALTVD  42387  trintALTVD  42389  undif3VD  42391  sbcssgVD  42392  csbingVD  42393  simplbi2comtVD  42397  onfrALTVD  42400  csbeq2gVD  42401  csbsngVD  42402  csbxpgVD  42403  csbresgVD  42404  csbrngVD  42405  csbima12gALTVD  42406  csbunigVD  42407  csbfv12gALTVD  42408  con5VD  42409  relopabVD  42410  19.41rgVD  42411  2pm13.193VD  42412  hbimpgVD  42413  hbalgVD  42414  hbexgVD  42415  ax6e2eqVD  42416  ax6e2ndVD  42417  ax6e2ndeqVD  42418  2sb5ndVD  42419  2uasbanhVD  42420  e2ebindVD  42421  sb5ALTVD  42422  vk15.4jVD  42423  notnotrALTVD  42424  con3ALTVD  42425  sspwimpVD  42428  sspwimpcfVD  42430  suctrALTcfVD  42432