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  704  mp3an3  1458  merco2  1743  equs4v  2007  alequexv  2008  equcomiv  2021  equcomi  2024  equvinva  2037  aeveq  2065  spimt  2394  equs4  2424  axc15  2430  2ax6elem  2478  dfeumo  2540  mo4  2570  sbcth  3738  sbcth2  3816  ssun3  4109  ssun4  4110  elpreqprlem  4797  uniintsn  4915  sepexlem  5221  axprlem2  5353  axprlem4  5355  axpr  5356  axprlem1OLD  5357  axprlem3OLD  5358  axprlem4OLD  5359  axprlem5OLD  5360  axprOLD  5361  axprglem  5365  exel  5373  rext  5387  exss  5402  snopeqop  5447  propssopi  5449  uniopel  5457  opthhausdorff  5458  opthhausdorff0  5459  wefrc  5612  relopabi  5765  relop  5792  dmrnssfld  5916  iss  5987  sofld  6138  ordun  6416  funimass2  6568  fvbr0  6854  fvmptg  6933  funsndifnop  7094  ov3  7519  elovmpo  7601  dford5  7727  limsssuc  7790  tfisi  7799  finds1  7839  frxp  8066  frxp2  8084  frxp3  8091  dfrecs3  8302  tfrlem1  8305  oaordi  8471  oaword2  8478  omeulem1  8507  oeworde  8519  oelim2  8521  nnaordi  8544  oaabs2  8575  limenpsi  9080  dif1en  9086  ordunifi  9190  fidomdm  9234  dffi3  9334  oismo  9445  wdom2d  9485  wdomima2g  9491  epnsym  9521  suc11reg  9531  elom3  9560  cantnfval2  9581  rankunb  9765  rankval4  9782  karden  9810  cardsn  9884  cardlim  9887  cardprclem  9894  fseqdom  9939  dfac12lem3  10059  kmlem2  10065  kmlem10  10073  cflim2  10176  cfslb2n  10181  fin23lem27  10241  fin23lem17  10251  axcc3  10351  axcc4  10352  acncc  10353  domtriomlem  10355  axdclem2  10433  imadomg  10447  alephval2  10486  alephreg  10496  axextnd  10505  fpwwe2lem9  10553  pwfseq  10578  gch2  10589  axgroth3  10745  inaprc  10750  nlt1pi  10820  indpi  10821  1re  11135  mul02lem2  11314  addrid  11317  fimaxre  12091  fiminre  12094  supaddc  12114  supmul1  12116  rimul  12141  nnge1  12196  zneo  12603  ltweuz  13914  hashrabsn1  14327  hashf1lem2  14409  hash2pwpr  14429  climuni  15505  fsum2d  15724  fsumabs  15755  fsumrlim  15765  fsumo1  15766  fsumiun  15775  fprod2d  15937  efne0d  16053  efne0OLD  16055  ruclem13  16200  dvdslelem  16269  mod2eq1n2dvds  16307  nn0o1gt2  16341  divalglem0  16353  lcmfnnval  16584  prmreclem2  16879  prmreclem3  16880  mreexexd  17605  coaval  18026  xpcco  18140  pltirr  18290  frgpnabllem1  19839  ablfac1eulem  20040  prmgrpsimpgd  20082  mdetunilem9  22603  mretopd  23075  fiuncmp  23387  ptcmpfi  23796  filtop  23838  supnfcls  24003  flimfnfcls  24011  alexsubALTlem2  24031  alexsubALTlem4  24033  trust  24212  rectbntr0  24816  fsumcn  24855  ovoliunlem3  25489  ovolicc2lem4  25505  dyadmax  25583  vitali  25598  itgfsum  25812  dvmptfsum  25960  fta1g  26153  fta1  26292  aannenlem1  26312  aalioulem3  26318  logltb  26582  logdmn0  26622  ang180lem2  26792  angpined  26812  mumullem2  27161  lgsqrmodndvds  27334  gausslemma2dlem0i  27345  2lgs  27388  dchrisum0re  27494  chpdifbnd  27536  pntrlog2bnd  27565  pntibndlem3  27573  pnt3  27593  nofv  27639  nomaxmo  27680  nominmo  27681  noprc  27766  madebday  27910  addsproplem7  27985  negsproplem7  28044  elons2  28268  nbgrval  29423  vtxdginducedm1fi  29631  upgrewlkle2  29693  hiidge0  31187  chsupval  31424  chsupcl  31429  chsupss  31431  ococin  31497  chsupval2  31499  ssjo  31536  h1de2i  31642  pjss2i  31769  pjssmii  31770  sto2i  32326  stge1i  32327  stle0i  32328  stlei  32329  stlesi  32330  stm1i  32332  staddi  32335  stadd3i  32337  golem1  32360  stcltrlem1  32365  mdexchi  32424  chirred  32484  atabsi  32490  abrexdomjm  32595  iocinif  32873  cycpmcl  33197  elrgspnsubrunlem2  33329  voliune  34413  volfiniune  34414  probdif  34604  bnj849  35107  axprALT2  35290  onvf1odlem4  35334  onvf1od  35335  kur14lem9  35442  gonarlem  35622  gonar  35623  goalrlem  35624  goalr  35625  sscoid  36139  limsucncmpi  36673  axtco1from2  36703  axtcond  36706  bj-nnf-spime  37118  bj-axc10  37136  bj-alequex  37137  bj-spimtv  37147  bj-moeub  37202  bj-exlimvmpi  37264  bj-exlimmpi  37265  bj-restpw  37450  bj-isrvec  37654  finxpreclem4  37756  domalom  37766  wl-isseteq  37867  wl-embant  37881  wl-orel12  37882  wl-euequf  37945  poimirlem9  37996  abrexdom  38097  heiborlem10  38187  dvrunz  38321  iss2  38711  equcomi1  39392  ax12eq  39433  ax12el  39434  ax12inda  39440  ax12v2-o  39441  cvrnrefN  39774  pmod1i  40340  pmodN  40342  osumcllem11N  40458  pexmidlem8N  40469  pl42lem3N  40473  cdleme18b  40784  dochexmidlem8  41959  imadomfi  42487  sticksstones3  42633  sn-axprlem3  42705  sn-exelALT  42706  sn-1ne2  42748  remul02  42882  sn-0tie0  42941  pellexlem3  43276  pell1234qrne0  43298  hbtlem6  43574  onsucelab  43708  omabs2  43777  nadd2rabex  43831  or3or  44467  isotone1  44492  isotone2  44493  clsf2  44570  ismnushort  44745  radcnvrat  44758  3impexpbicom  44924  sb5ALT  44969  eexinst01  44970  ax6e2eq  45001  sineq0ALT  45380  tcfr  45407  ssclaxsep  45426  omssaxinf2  45432  nregmodel  45461  fzisoeu  45748  ovnsubaddlem2  47014  ormklocald  47319  natlocalincr  47321  tannpoly  47353  funressnfv  47506  faovcl  47663  sprsymrelfo  47972  clnbgrval  48313  gpgedgiov  48556  gpgedg2ov  48557  gpgedg2iv  48558  pgnioedg1  48599  pgnioedg2  48600  pgnioedg3  48601  pgnioedg4  48602  pgnioedg5  48603  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  pgnbgreunbgrlem5lem1  48611  pgnbgreunbgrlem5lem2  48612  cznnring  48753  zlmodzxznm  48988  elbigolo1  49048  dignn0flhalflem1  49106  nn0sumshdig  49114  rrx2xpref1o  49209  fonex  49357  vsetrec  50193