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  696  mp3an3  1446  merco2  1730  equs4v  1995  alequexv  1996  equcomiv  2009  equcomi  2012  equvinva  2025  aeveq  2051  spimt  2379  equs4  2409  axc15  2415  2ax6elem  2463  dfeumo  2525  mo4  2554  pm13.183  3652  sbcth  3789  sbcth2  3875  ssun3  4173  ssun4  4174  elpreqprlem  4867  uniintsn  4990  axprlem1  5422  axprlem2  5423  axprlem3  5424  axprlem4  5425  axprlem5  5426  axpr  5427  exel  5434  rext  5449  exss  5464  snopeqop  5507  propssopi  5509  uniopel  5517  opthhausdorff  5518  opthhausdorff0  5519  wefrc  5671  relopabi  5823  relop  5852  dmrnssfld  5972  iss  6039  sofld  6191  ordun  6473  funimass2  6635  fvbr0  6923  fvmptg  7000  funsndifnop  7158  ov3  7582  elovmpo  7664  dford5  7785  limsssuc  7853  tfisi  7862  finds1  7905  frxp  8129  frxp2  8147  frxp3  8154  wfrlem5OLD  8332  wfrlem16OLD  8343  dfrecs3  8391  dfrecs3OLD  8392  tfrlem1  8395  oaordi  8565  oaword2  8572  omeulem1  8601  oeworde  8612  oelim2  8614  nnaordi  8637  oaabs2  8668  0domgOLD  9124  limenpsi  9175  dif1en  9183  dif1enOLD  9185  enp1iOLD  9303  findcard2OLD  9307  ordunifi  9316  fidomdm  9353  dffi3  9454  oismo  9563  wdom2d  9603  wdomima2g  9609  epnsym  9632  suc11reg  9642  elom3  9671  cantnfval2  9692  rankunb  9873  rankval4  9890  karden  9918  cardsn  9992  cardlim  9995  cardprclem  10002  fseqdom  10049  dfac12lem3  10168  kmlem2  10174  kmlem10  10182  cflim2  10286  cfslb2n  10291  fin23lem27  10351  fin23lem17  10361  axcc3  10461  axcc4  10462  acncc  10463  domtriomlem  10465  axdclem2  10543  imadomg  10557  alephval2  10595  alephreg  10605  axextnd  10614  fpwwe2lem9  10662  pwfseq  10687  gch2  10698  axgroth3  10854  inaprc  10859  nlt1pi  10929  indpi  10930  1re  11244  mul02lem2  11421  addrid  11424  fimaxre  12188  fiminre  12191  supaddc  12211  supmul1  12213  inelr  12232  rimul  12233  nnge1  12270  zneo  12675  ltweuz  13958  hashrabsn1  14365  hashf1lem2  14449  hash2pwpr  14469  climuni  15528  fsum2d  15749  fsumabs  15779  fsumrlim  15789  fsumo1  15790  fsumiun  15799  fprod2d  15957  efne0  16073  ruclem13  16218  dvdslelem  16285  mod2eq1n2dvds  16323  nn0o1gt2  16357  divalglem0  16369  lcmfnnval  16594  prmreclem2  16885  prmreclem3  16886  mreexexd  17627  coaval  18056  xpcco  18173  pltirr  18326  frgpnabllem1  19832  ablfac1eulem  20033  prmgrpsimpgd  20075  mdetunilem9  22552  mretopd  23026  fiuncmp  23338  ptcmpfi  23747  filtop  23789  supnfcls  23954  flimfnfcls  23962  alexsubALTlem2  23982  alexsubALTlem4  23984  trust  24164  rectbntr0  24778  fsumcn  24818  ovoliunlem3  25463  ovolicc2lem4  25479  dyadmax  25557  vitali  25572  itgfsum  25786  dvmptfsum  25937  fta1g  26134  fta1  26273  aannenlem1  26293  aalioulem3  26299  logltb  26564  logdmn0  26604  ang180lem2  26772  angpined  26792  mumullem2  27142  lgsqrmodndvds  27316  gausslemma2dlem0i  27327  2lgs  27370  dchrisum0re  27476  chpdifbnd  27518  pntrlog2bnd  27547  pntibndlem3  27555  pnt3  27575  nofv  27620  nomaxmo  27661  nominmo  27662  noprc  27742  madebday  27856  addsproplem7  27922  negsproplem7  27976  elons2  28185  nbgrval  29205  vtxdginducedm1fi  29414  upgrewlkle2  29476  hiidge0  30964  chsupval  31201  chsupcl  31206  chsupss  31208  ococin  31274  chsupval2  31276  ssjo  31313  h1de2i  31419  pjss2i  31546  pjssmii  31547  sto2i  32103  stge1i  32104  stle0i  32105  stlei  32106  stlesi  32107  stm1i  32109  staddi  32112  stadd3i  32114  golem1  32137  stcltrlem1  32142  mdexchi  32201  chirred  32261  atabsi  32267  abrexdomjm  32359  iocinif  32606  cycpmcl  32894  voliune  33918  volfiniune  33919  probdif  34110  bnj849  34626  kur14lem9  34894  gonarlem  35074  gonar  35075  goalrlem  35076  goalr  35077  sscoid  35579  limsucncmpi  35999  bj-axc10  36330  bj-alequex  36331  bj-spimtv  36341  bj-moeub  36396  bj-exlimvmpi  36459  bj-exlimmpi  36460  bj-restpw  36641  bj-isrvec  36843  finxpreclem4  36943  domalom  36953  wl-embant  37047  wl-orel12  37048  wl-euequf  37111  poimirlem9  37172  abrexdom  37273  heiborlem10  37363  dvrunz  37497  iss2  37885  equcomi1  38441  ax12eq  38482  ax12el  38483  ax12inda  38489  ax12v2-o  38490  cvrnrefN  38823  pmod1i  39390  pmodN  39392  osumcllem11N  39508  pexmidlem8N  39519  pl42lem3N  39523  cdleme18b  39834  dochexmidlem8  41009  imadomfi  41542  sticksstones3  41689  sn-axprlem3  41774  sn-exelALT  41775  sn-1ne2  41905  efne0d  41973  remul02  42025  sn-0tie0  42059  pellexlem3  42316  pell1234qrne0  42338  hbtlem6  42618  onsucelab  42757  omabs2  42826  nadd2rabex  42880  or3or  43518  isotone1  43543  isotone2  43544  clsf2  43621  ismnushort  43803  radcnvrat  43816  3impexpbicom  43983  sb5ALT  44029  eexinst01  44030  ax6e2eq  44061  sineq0ALT  44441  fzisoeu  44745  ovnsubaddlem2  46022  natlocalincr  46325  tworepnotupword  46335  funressnfv  46488  faovcl  46643  sprsymrelfo  46900  clnbgrval  47225  cznnring  47436  zlmodzxznm  47677  elbigolo1  47742  dignn0flhalflem1  47800  nn0sumshdig  47808  rrx2xpref1o  47903  vsetrec  48246