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  2390  equs4  2420  axc15  2426  2ax6elem  2474  dfeumo  2536  mo4  2566  sbcth  3743  sbcth2  3822  ssun3  4120  ssun4  4121  elpreqprlem  4809  uniintsn  4927  sepexlem  5234  axprlem2  5366  axprlem4  5368  axpr  5369  axprlem1OLD  5370  axprlem3OLD  5371  axprlem4OLD  5372  axprlem5OLD  5373  axprOLD  5374  axprglem  5378  exel  5386  rext  5400  exss  5415  snopeqop  5460  propssopi  5462  uniopel  5470  opthhausdorff  5471  opthhausdorff0  5472  wefrc  5625  relopabi  5778  relop  5805  dmrnssfld  5929  iss  6000  sofld  6151  ordun  6429  funimass2  6581  fvbr0  6867  fvmptg  6945  funsndifnop  7105  ov3  7530  elovmpo  7612  dford5  7738  limsssuc  7801  tfisi  7810  finds1  7850  frxp  8076  frxp2  8094  frxp3  8101  dfrecs3  8312  tfrlem1  8315  oaordi  8481  oaword2  8488  omeulem1  8517  oeworde  8529  oelim2  8531  nnaordi  8554  oaabs2  8585  limenpsi  9090  dif1en  9096  ordunifi  9200  fidomdm  9244  dffi3  9344  oismo  9455  wdom2d  9495  wdomima2g  9501  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  11323  addrid  11326  fimaxre  12100  fiminre  12103  supaddc  12123  supmul1  12125  rimul  12150  nnge1  12205  zneo  12612  ltweuz  13923  hashrabsn1  14336  hashf1lem2  14418  hash2pwpr  14438  climuni  15514  fsum2d  15733  fsumabs  15764  fsumrlim  15774  fsumo1  15775  fsumiun  15784  fprod2d  15946  efne0d  16062  efne0OLD  16064  ruclem13  16209  dvdslelem  16278  mod2eq1n2dvds  16316  nn0o1gt2  16350  divalglem0  16362  lcmfnnval  16593  prmreclem2  16888  prmreclem3  16889  mreexexd  17614  coaval  18035  xpcco  18149  pltirr  18299  frgpnabllem1  19848  ablfac1eulem  20049  prmgrpsimpgd  20091  mdetunilem9  22585  mretopd  23057  fiuncmp  23369  ptcmpfi  23778  filtop  23820  supnfcls  23985  flimfnfcls  23993  alexsubALTlem2  24013  alexsubALTlem4  24015  trust  24194  rectbntr0  24798  fsumcn  24837  ovoliunlem3  25471  ovolicc2lem4  25487  dyadmax  25565  vitali  25580  itgfsum  25794  dvmptfsum  25942  fta1g  26135  fta1  26274  aannenlem1  26294  aalioulem3  26300  logltb  26564  logdmn0  26604  ang180lem2  26774  angpined  26794  mumullem2  27143  lgsqrmodndvds  27316  gausslemma2dlem0i  27327  2lgs  27370  dchrisum0re  27476  chpdifbnd  27518  pntrlog2bnd  27547  pntibndlem3  27555  pnt3  27575  nofv  27621  nomaxmo  27662  nominmo  27663  noprc  27748  madebday  27892  addsproplem7  27967  negsproplem7  28026  elons2  28250  nbgrval  29405  vtxdginducedm1fi  29613  upgrewlkle2  29675  hiidge0  31169  chsupval  31406  chsupcl  31411  chsupss  31413  ococin  31479  chsupval2  31481  ssjo  31518  h1de2i  31624  pjss2i  31751  pjssmii  31752  sto2i  32308  stge1i  32309  stle0i  32310  stlei  32311  stlesi  32312  stm1i  32314  staddi  32317  stadd3i  32319  golem1  32342  stcltrlem1  32347  mdexchi  32406  chirred  32466  atabsi  32472  abrexdomjm  32577  iocinif  32854  cycpmcl  33177  elrgspnsubrunlem2  33309  voliune  34373  volfiniune  34374  probdif  34564  bnj849  35067  axprALT2  35253  onvf1odlem4  35288  onvf1od  35289  kur14lem9  35396  gonarlem  35576  gonar  35577  goalrlem  35578  goalr  35579  sscoid  36093  limsucncmpi  36627  axtco1from2  36657  axtcond  36660  bj-nnf-spime  37072  bj-axc10  37090  bj-alequex  37091  bj-spimtv  37101  bj-moeub  37156  bj-exlimvmpi  37218  bj-exlimmpi  37219  bj-restpw  37404  bj-isrvec  37608  finxpreclem4  37710  domalom  37720  wl-isseteq  37821  wl-embant  37835  wl-orel12  37836  wl-euequf  37899  poimirlem9  37950  abrexdom  38051  heiborlem10  38141  dvrunz  38275  iss2  38665  equcomi1  39346  ax12eq  39387  ax12el  39388  ax12inda  39394  ax12v2-o  39395  cvrnrefN  39728  pmod1i  40294  pmodN  40296  osumcllem11N  40412  pexmidlem8N  40423  pl42lem3N  40427  cdleme18b  40738  dochexmidlem8  41913  imadomfi  42441  sticksstones3  42587  sn-axprlem3  42659  sn-exelALT  42660  sn-1ne2  42703  remul02  42837  sn-0tie0  42896  pellexlem3  43259  pell1234qrne0  43281  hbtlem6  43557  onsucelab  43691  omabs2  43760  nadd2rabex  43814  or3or  44450  isotone1  44475  isotone2  44476  clsf2  44553  ismnushort  44728  radcnvrat  44741  3impexpbicom  44907  sb5ALT  44952  eexinst01  44953  ax6e2eq  44984  sineq0ALT  45363  tcfr  45390  ssclaxsep  45409  omssaxinf2  45415  nregmodel  45444  fzisoeu  45733  ovnsubaddlem2  46999  ormklocald  47304  natlocalincr  47306  tannpoly  47338  funressnfv  47491  faovcl  47648  sprsymrelfo  47957  clnbgrval  48298  gpgedgiov  48541  gpgedg2ov  48542  gpgedg2iv  48543  pgnioedg1  48584  pgnioedg2  48585  pgnioedg3  48586  pgnioedg4  48587  pgnioedg5  48588  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  cznnring  48738  zlmodzxznm  48973  elbigolo1  49033  dignn0flhalflem1  49091  nn0sumshdig  49099  rrx2xpref1o  49194  fonex  49342  vsetrec  50178