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  697  mp3an3  1450  merco2  1734  equs4v  1999  alequexv  2000  equcomiv  2013  equcomi  2016  equvinva  2029  aeveq  2056  spimt  2388  equs4  2418  axc15  2424  2ax6elem  2472  dfeumo  2534  mo4  2563  sbcth  3813  sbcth2  3900  ssun3  4197  ssun4  4198  elpreqprlem  4890  uniintsn  5013  axprlem1  5444  axprlem2  5445  axprlem3  5446  axprlem4  5447  axprlem5  5448  axpr  5449  exel  5456  rext  5471  exss  5486  snopeqop  5529  propssopi  5531  uniopel  5539  opthhausdorff  5540  opthhausdorff0  5541  wefrc  5693  relopabi  5845  relop  5874  dmrnssfld  5995  iss  6063  sofld  6217  ordun  6498  funimass2  6660  fvbr0  6948  fvmptg  7025  funsndifnop  7183  ov3  7609  elovmpo  7691  dford5  7815  limsssuc  7883  tfisi  7892  finds1  7935  frxp  8163  frxp2  8181  frxp3  8188  wfrlem5OLD  8365  wfrlem16OLD  8376  dfrecs3  8424  dfrecs3OLD  8425  tfrlem1  8428  oaordi  8598  oaword2  8605  omeulem1  8634  oeworde  8645  oelim2  8647  nnaordi  8670  oaabs2  8701  0domgOLD  9163  limenpsi  9214  dif1en  9222  dif1enOLD  9224  enp1iOLD  9338  ordunifi  9350  fidomdm  9398  dffi3  9496  oismo  9605  wdom2d  9645  wdomima2g  9651  epnsym  9674  suc11reg  9684  elom3  9713  cantnfval2  9734  rankunb  9915  rankval4  9932  karden  9960  cardsn  10034  cardlim  10037  cardprclem  10044  fseqdom  10091  dfac12lem3  10211  kmlem2  10217  kmlem10  10225  cflim2  10328  cfslb2n  10333  fin23lem27  10393  fin23lem17  10403  axcc3  10503  axcc4  10504  acncc  10505  domtriomlem  10507  axdclem2  10585  imadomg  10599  alephval2  10637  alephreg  10647  axextnd  10656  fpwwe2lem9  10704  pwfseq  10729  gch2  10740  axgroth3  10896  inaprc  10901  nlt1pi  10971  indpi  10972  1re  11286  mul02lem2  11463  addrid  11466  fimaxre  12235  fiminre  12238  supaddc  12258  supmul1  12260  inelr  12279  rimul  12280  nnge1  12317  zneo  12722  ltweuz  14008  hashrabsn1  14419  hashf1lem2  14501  hash2pwpr  14521  climuni  15594  fsum2d  15815  fsumabs  15845  fsumrlim  15855  fsumo1  15856  fsumiun  15865  fprod2d  16023  efne0  16139  ruclem13  16284  dvdslelem  16351  mod2eq1n2dvds  16389  nn0o1gt2  16423  divalglem0  16435  lcmfnnval  16665  prmreclem2  16959  prmreclem3  16960  mreexexd  17701  coaval  18130  xpcco  18247  pltirr  18400  frgpnabllem1  19910  ablfac1eulem  20111  prmgrpsimpgd  20153  mdetunilem9  22640  mretopd  23114  fiuncmp  23426  ptcmpfi  23835  filtop  23877  supnfcls  24042  flimfnfcls  24050  alexsubALTlem2  24070  alexsubALTlem4  24072  trust  24252  rectbntr0  24866  fsumcn  24906  ovoliunlem3  25551  ovolicc2lem4  25567  dyadmax  25645  vitali  25660  itgfsum  25874  dvmptfsum  26025  fta1g  26221  fta1  26360  aannenlem1  26380  aalioulem3  26386  logltb  26651  logdmn0  26691  ang180lem2  26862  angpined  26882  mumullem2  27232  lgsqrmodndvds  27406  gausslemma2dlem0i  27417  2lgs  27460  dchrisum0re  27566  chpdifbnd  27608  pntrlog2bnd  27637  pntibndlem3  27645  pnt3  27665  nofv  27711  nomaxmo  27752  nominmo  27753  noprc  27833  madebday  27947  addsproplem7  28017  negsproplem7  28075  elons2  28290  nbgrval  29362  vtxdginducedm1fi  29571  upgrewlkle2  29633  hiidge0  31121  chsupval  31358  chsupcl  31363  chsupss  31365  ococin  31431  chsupval2  31433  ssjo  31470  h1de2i  31576  pjss2i  31703  pjssmii  31704  sto2i  32260  stge1i  32261  stle0i  32262  stlei  32263  stlesi  32264  stm1i  32266  staddi  32269  stadd3i  32271  golem1  32294  stcltrlem1  32299  mdexchi  32358  chirred  32418  atabsi  32424  abrexdomjm  32526  iocinif  32778  cycpmcl  33101  voliune  34185  volfiniune  34186  probdif  34377  bnj849  34893  kur14lem9  35174  gonarlem  35354  gonar  35355  goalrlem  35356  goalr  35357  sscoid  35869  limsucncmpi  36358  bj-axc10  36697  bj-alequex  36698  bj-spimtv  36708  bj-moeub  36763  bj-exlimvmpi  36825  bj-exlimmpi  36826  bj-restpw  37006  bj-isrvec  37208  finxpreclem4  37308  domalom  37318  wl-embant  37412  wl-orel12  37413  wl-euequf  37476  poimirlem9  37537  abrexdom  37638  heiborlem10  37728  dvrunz  37862  iss2  38248  equcomi1  38804  ax12eq  38845  ax12el  38846  ax12inda  38852  ax12v2-o  38853  cvrnrefN  39186  pmod1i  39753  pmodN  39755  osumcllem11N  39871  pexmidlem8N  39882  pl42lem3N  39886  cdleme18b  40197  dochexmidlem8  41372  imadomfi  41907  sticksstones3  42053  sn-axprlem3  42159  sn-exelALT  42160  sn-1ne2  42202  efne0d  42262  remul02  42314  sn-0tie0  42348  pellexlem3  42724  pell1234qrne0  42746  hbtlem6  43026  onsucelab  43165  omabs2  43234  nadd2rabex  43288  or3or  43925  isotone1  43950  isotone2  43951  clsf2  44028  ismnushort  44210  radcnvrat  44223  3impexpbicom  44390  sb5ALT  44436  eexinst01  44437  ax6e2eq  44468  sineq0ALT  44848  fzisoeu  45149  ovnsubaddlem2  46426  natlocalincr  46729  tworepnotupword  46739  funressnfv  46892  faovcl  47047  sprsymrelfo  47303  clnbgrval  47628  cznnring  47903  zlmodzxznm  48144  elbigolo1  48209  dignn0flhalflem1  48267  nn0sumshdig  48275  rrx2xpref1o  48370  vsetrec  48713