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  1737  equs4v  2006  alequexv  2007  equcomiv  2021  equcomi  2024  equvinva  2037  aeveq  2061  spsbeOLD  2089  spimt  2404  equs4  2438  axc15  2444  2ax6elem  2493  dfeumo  2619  mo4  2650  pm13.183  3661  pm13.183OLD  3662  sbcth  3789  sbcth2  3869  ssun3  4152  ssun4  4153  elpreqprlem  4798  uniintsn  4915  axprlem1  5326  axprlem2  5327  axprlem3  5328  axprlem4  5329  axprlem5  5330  axpr  5331  rext  5343  exss  5357  snopeqop  5398  propssopi  5400  uniopel  5408  opthhausdorff  5409  opthhausdorff0  5410  wefrc  5551  relopabi  5696  relop  5723  dmrnssfld  5843  iss  5905  sofld  6046  ordun  6294  funimass2  6439  fvbr0  6699  fvmptg  6768  funsndifnop  6915  fovcl  7281  ov3  7313  elovmpo  7392  limsssuc  7567  tfisi  7575  finds1  7613  frxp  7822  wfrlem5  7961  wfrlem16  7972  dfrecs3  8011  tfrlem1  8014  oaordi  8174  oaword2  8181  omeulem1  8210  oeworde  8221  oelim2  8223  nnaordi  8246  oaabs2  8274  0domg  8646  limenpsi  8694  enp1i  8755  findcard2  8760  ordunifi  8770  fidomdm  8803  dffi3  8897  oismo  9006  wdom2d  9046  wdomima2g  9052  epnsym  9074  suc11reg  9084  elom3  9113  cantnfval2  9134  rankunb  9281  rankval4  9298  karden  9326  cardsn  9400  cardlim  9403  cardprclem  9410  fseqdom  9454  dfac12lem3  9573  kmlem2  9579  kmlem10  9587  cflim2  9687  cfslb2n  9692  fin23lem27  9752  fin23lem17  9762  axcc3  9862  axcc4  9863  acncc  9864  domtriomlem  9866  axdclem2  9944  imadomg  9958  alephval2  9996  alephreg  10006  axextnd  10015  fpwwe2lem10  10063  pwfseq  10088  gch2  10099  axgroth3  10255  inaprc  10260  nlt1pi  10330  indpi  10331  1re  10643  mul02lem2  10819  addid1  10822  fimaxre  11586  fimaxreOLD  11587  fiminre  11590  supaddc  11610  supmul1  11612  inelr  11630  rimul  11631  nnge1  11668  nnne0  11674  zneo  12068  ltweuz  13332  hashrabsn1  13738  hashf1lem2  13817  hash2pwpr  13837  climuni  14911  fsum2d  15128  fsumabs  15158  fsumrlim  15168  fsumo1  15169  fsumiun  15178  fprod2d  15337  efne0  15452  ruclem13  15597  dvdslelem  15661  mod2eq1n2dvds  15698  nn0o1gt2  15734  divalglem0  15746  lcmfnnval  15970  prmreclem2  16255  prmreclem3  16256  mreexexd  16921  coaval  17330  xpcco  17435  pltirr  17575  frgpnabllem1  18995  ablfac1eulem  19196  prmgrpsimpgd  19238  mdetunilem9  21231  mretopd  21702  fiuncmp  22014  ptcmpfi  22423  filtop  22465  supnfcls  22630  flimfnfcls  22638  alexsubALTlem2  22658  alexsubALTlem4  22660  trust  22840  rectbntr0  23442  fsumcn  23480  ovoliunlem3  24107  ovolicc2lem4  24123  dyadmax  24201  vitali  24216  itgfsum  24429  dvmptfsum  24574  fta1g  24763  fta1  24899  aannenlem1  24919  aalioulem3  24925  logltb  25185  logdmn0  25225  ang180lem2  25390  angpined  25410  mumullem2  25759  lgsqrmodndvds  25931  gausslemma2dlem0i  25942  2lgs  25985  dchrisum0re  26091  chpdifbnd  26133  pntrlog2bnd  26162  pntibndlem3  26170  pnt3  26190  nbgrval  27120  vtxdginducedm1fi  27328  upgrewlkle2  27390  hiidge0  28877  chsupval  29114  chsupcl  29119  chsupss  29121  ococin  29187  chsupval2  29189  ssjo  29226  h1de2i  29332  pjss2i  29459  pjssmii  29460  sto2i  30016  stge1i  30017  stle0i  30018  stlei  30019  stlesi  30020  stm1i  30022  staddi  30025  stadd3i  30027  golem1  30050  stcltrlem1  30055  mdexchi  30114  chirred  30174  atabsi  30180  abrexdomjm  30269  iocinif  30506  cycpmcl  30760  voliune  31490  volfiniune  31491  probdif  31680  bnj849  32199  kur14lem9  32463  gonarlem  32643  gonar  32644  goalrlem  32645  goalr  32646  dford5  32959  nofv  33166  nomaxmo  33203  noprc  33251  sscoid  33376  limsucncmpi  33795  bj-axc10  34107  bj-alequex  34108  bj-spimtv  34118  bj-moeub  34175  bj-exlimvmpi  34229  bj-exlimmpi  34230  bj-restpw  34385  finxpreclem4  34677  domalom  34687  wl-embant  34752  wl-orel12  34753  wl-euequf  34812  poimirlem9  34903  abrexdom  35007  heiborlem10  35100  dvrunz  35234  iss2  35603  equcomi1  36038  ax12eq  36079  ax12el  36080  ax12inda  36086  ax12v2-o  36087  cvrnrefN  36420  pmod1i  36986  pmodN  36988  osumcllem11N  37104  pexmidlem8N  37115  pl42lem3N  37119  cdleme18b  37430  dochexmidlem8  38605  sn-axprlem3  39116  sn-el  39117  sn-1ne2  39165  remul02  39242  pellexlem3  39435  pell1234qrne0  39457  hbtlem6  39736  or3or  40378  isotone1  40405  isotone2  40406  clsf2  40483  radcnvrat  40653  3impexpbicom  40820  sb5ALT  40866  eexinst01  40867  ax6e2eq  40898  sineq0ALT  41278  fzisoeu  41574  ovnsubaddlem2  42860  funressnfv  43285  faovcl  43406  sprsymrelfo  43666  cznnring  44234  zlmodzxznm  44559  elbigolo1  44624  dignn0flhalflem1  44682  nn0sumshdig  44690  rrx2xpref1o  44712  vsetrec  44812