Theorem in1 43317

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

Syntax hints:   → wi 4  (   wvd1 43315

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 43316

This theorem is referenced by:  vd12  43346  vd13  43347  gen11nv  43363  gen12  43364  exinst11  43372  e1a  43373  el1  43374  e223  43381  e111  43420  e1111  43421  el2122old  43465  el12  43472  el123  43510  un0.1  43525  trsspwALT  43564  sspwtr  43567  pwtrVD  43570  pwtrrVD  43571  snssiALTVD  43573  snsslVD  43575  snelpwrVD  43577  unipwrVD  43578  sstrALT2VD  43580  suctrALT2VD  43582  elex2VD  43584  elex22VD  43585  eqsbc2VD  43586  zfregs2VD  43587  tpid3gVD  43588  en3lplem1VD  43589  en3lplem2VD  43590  en3lpVD  43591  3ornot23VD  43593  orbi1rVD  43594  3orbi123VD  43596  sbc3orgVD  43597  19.21a3con13vVD  43598  exbirVD  43599  exbiriVD  43600  rspsbc2VD  43601  3impexpVD  43602  3impexpbicomVD  43603  sbcoreleleqVD  43605  tratrbVD  43607  al2imVD  43608  syl5impVD  43609  ssralv2VD  43612  ordelordALTVD  43613  equncomVD  43614  imbi12VD  43619  imbi13VD  43620  sbcim2gVD  43621  sbcbiVD  43622  trsbcVD  43623  truniALTVD  43624  trintALTVD  43626  undif3VD  43628  sbcssgVD  43629  csbingVD  43630  simplbi2comtVD  43634  onfrALTVD  43637  csbeq2gVD  43638  csbsngVD  43639  csbxpgVD  43640  csbresgVD  43641  csbrngVD  43642  csbima12gALTVD  43643  csbunigVD  43644  csbfv12gALTVD  43645  con5VD  43646  relopabVD  43647  19.41rgVD  43648  2pm13.193VD  43649  hbimpgVD  43650  hbalgVD  43651  hbexgVD  43652  ax6e2eqVD  43653  ax6e2ndVD  43654  ax6e2ndeqVD  43655  2sb5ndVD  43656  2uasbanhVD  43657  e2ebindVD  43658  sb5ALTVD  43659  vk15.4jVD  43660  notnotrALTVD  43661  con3ALTVD  43662  sspwimpVD  43665  sspwimpcfVD  43667  suctrALTcfVD  43669