Theorem mpi 20

Description: A nested modus ponens inference. Inference associated with com12 32. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Stefan Allan, 20-Mar-2006.)

Hypotheses

Ref	Expression
mpi.1	⊢ 𝜓
mpi.2	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
mpi	⊢ (𝜑 → 𝜒)

Proof of Theorem mpi

Step	Hyp	Ref	Expression
1		mpi.1	. . 3 ⊢ 𝜓
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝜓)
3		mpi.2	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  mpisyl  21  syl6mpi  67  mp2ani  699  mp3an3  1453  merco2  1738  equs4v  2002  alequexv  2003  equcomiv  2016  equcomi  2019  equvinva  2032  aeveq  2060  spimt  2391  equs4  2421  axc15  2427  2ax6elem  2475  dfeumo  2537  mo4  2567  sbcth  3757  sbcth2  3836  ssun3  4134  ssun4  4135  elpreqprlem  4824  uniintsn  4942  sepexlem  5246  axprlem1  5370  axprlem2  5371  axprlem4  5373  axpr  5374  axprlem3OLD  5375  axprlem4OLD  5376  axprlem5OLD  5377  axprOLD  5378  axprglem  5382  exel  5390  rext  5403  exss  5418  snopeqop  5462  propssopi  5464  uniopel  5472  opthhausdorff  5473  opthhausdorff0  5474  wefrc  5626  relopabi  5779  relop  5807  dmrnssfld  5931  iss  6002  sofld  6153  ordun  6431  funimass2  6583  fvbr0  6869  fvmptg  6947  funsndifnop  7106  ov3  7531  elovmpo  7613  dford5  7739  limsssuc  7802  tfisi  7811  finds1  7851  frxp  8078  frxp2  8096  frxp3  8103  dfrecs3  8314  tfrlem1  8317  oaordi  8483  oaword2  8490  omeulem1  8519  oeworde  8531  oelim2  8533  nnaordi  8556  oaabs2  8587  limenpsi  9092  dif1en  9098  ordunifi  9202  fidomdm  9246  dffi3  9346  oismo  9457  wdom2d  9497  wdomima2g  9503  epnsym  9530  suc11reg  9540  elom3  9569  cantnfval2  9590  rankunb  9774  rankval4  9791  karden  9819  cardsn  9893  cardlim  9896  cardprclem  9903  fseqdom  9948  dfac12lem3  10068  kmlem2  10074  kmlem10  10082  cflim2  10185  cfslb2n  10190  fin23lem27  10250  fin23lem17  10260  axcc3  10360  axcc4  10361  acncc  10362  domtriomlem  10364  axdclem2  10442  imadomg  10456  alephval2  10495  alephreg  10505  axextnd  10514  fpwwe2lem9  10562  pwfseq  10587  gch2  10598  axgroth3  10754  inaprc  10759  nlt1pi  10829  indpi  10830  1re  11144  mul02lem2  11322  addrid  11325  fimaxre  12098  fiminre  12101  supaddc  12121  supmul1  12123  rimul  12148  nnge1  12185  zneo  12587  ltweuz  13896  hashrabsn1  14309  hashf1lem2  14391  hash2pwpr  14411  climuni  15487  fsum2d  15706  fsumabs  15736  fsumrlim  15746  fsumo1  15747  fsumiun  15756  fprod2d  15916  efne0d  16032  efne0OLD  16034  ruclem13  16179  dvdslelem  16248  mod2eq1n2dvds  16286  nn0o1gt2  16320  divalglem0  16332  lcmfnnval  16563  prmreclem2  16857  prmreclem3  16858  mreexexd  17583  coaval  18004  xpcco  18118  pltirr  18268  frgpnabllem1  19817  ablfac1eulem  20018  prmgrpsimpgd  20060  mdetunilem9  22579  mretopd  23051  fiuncmp  23363  ptcmpfi  23772  filtop  23814  supnfcls  23979  flimfnfcls  23987  alexsubALTlem2  24007  alexsubALTlem4  24009  trust  24188  rectbntr0  24792  fsumcn  24832  ovoliunlem3  25476  ovolicc2lem4  25492  dyadmax  25570  vitali  25585  itgfsum  25799  dvmptfsum  25950  fta1g  26146  fta1  26287  aannenlem1  26307  aalioulem3  26313  logltb  26580  logdmn0  26620  ang180lem2  26791  angpined  26811  mumullem2  27161  lgsqrmodndvds  27335  gausslemma2dlem0i  27346  2lgs  27389  dchrisum0re  27495  chpdifbnd  27537  pntrlog2bnd  27566  pntibndlem3  27574  pnt3  27594  nofv  27640  nomaxmo  27681  nominmo  27682  noprc  27767  madebday  27911  addsproplem7  27986  negsproplem7  28045  elons2  28269  nbgrval  29425  vtxdginducedm1fi  29634  upgrewlkle2  29696  hiidge0  31190  chsupval  31427  chsupcl  31432  chsupss  31434  ococin  31500  chsupval2  31502  ssjo  31539  h1de2i  31645  pjss2i  31772  pjssmii  31773  sto2i  32329  stge1i  32330  stle0i  32331  stlei  32332  stlesi  32333  stm1i  32335  staddi  32338  stadd3i  32340  golem1  32363  stcltrlem1  32368  mdexchi  32427  chirred  32487  atabsi  32493  abrexdomjm  32598  iocinif  32876  cycpmcl  33214  elrgspnsubrunlem2  33346  voliune  34411  volfiniune  34412  probdif  34602  bnj849  35105  axprALT2  35291  onvf1odlem4  35326  onvf1od  35327  kur14lem9  35434  gonarlem  35614  gonar  35615  goalrlem  35616  goalr  35617  sscoid  36131  limsucncmpi  36665  bj-axc10  37035  bj-alequex  37036  bj-spimtv  37046  bj-moeub  37101  bj-exlimvmpi  37163  bj-exlimmpi  37164  bj-restpw  37349  bj-isrvec  37553  finxpreclem4  37653  domalom  37663  wl-isseteq  37764  wl-embant  37769  wl-orel12  37770  wl-euequf  37833  poimirlem9  37884  abrexdom  37985  heiborlem10  38075  dvrunz  38209  iss2  38599  equcomi1  39280  ax12eq  39321  ax12el  39322  ax12inda  39328  ax12v2-o  39329  cvrnrefN  39662  pmod1i  40228  pmodN  40230  osumcllem11N  40346  pexmidlem8N  40357  pl42lem3N  40361  cdleme18b  40672  dochexmidlem8  41847  imadomfi  42376  sticksstones3  42522  sn-axprlem3  42594  sn-exelALT  42595  sn-1ne2  42639  remul02  42779  sn-0tie0  42825  pellexlem3  43192  pell1234qrne0  43214  hbtlem6  43490  onsucelab  43624  omabs2  43693  nadd2rabex  43747  or3or  44383  isotone1  44408  isotone2  44409  clsf2  44486  ismnushort  44661  radcnvrat  44674  3impexpbicom  44840  sb5ALT  44885  eexinst01  44886  ax6e2eq  44917  sineq0ALT  45296  tcfr  45323  ssclaxsep  45342  omssaxinf2  45348  nregmodel  45377  fzisoeu  45666  ovnsubaddlem2  46933  ormklocald  47236  natlocalincr  47238  tannpoly  47254  funressnfv  47407  faovcl  47564  sprsymrelfo  47861  clnbgrval  48186  gpgedgiov  48429  gpgedg2ov  48430  gpgedg2iv  48431  pgnioedg1  48472  pgnioedg2  48473  pgnioedg3  48474  pgnioedg4  48475  pgnioedg5  48476  pgnbgreunbgrlem2lem1  48478  pgnbgreunbgrlem2lem2  48479  pgnbgreunbgrlem2lem3  48480  pgnbgreunbgrlem5lem1  48484  pgnbgreunbgrlem5lem2  48485  cznnring  48626  zlmodzxznm  48861  elbigolo1  48921  dignn0flhalflem1  48979  nn0sumshdig  48987  rrx2xpref1o  49082  fonex  49230  vsetrec  50066