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  698  mp3an3  1452  merco2  1736  equs4v  2000  alequexv  2001  equcomiv  2014  equcomi  2017  equvinva  2030  aeveq  2057  spimt  2384  equs4  2414  axc15  2420  2ax6elem  2468  dfeumo  2530  mo4  2559  sbcth  3765  sbcth2  3844  ssun3  4139  ssun4  4140  elpreqprlem  4826  uniintsn  4945  sepexlem  5249  axprlem1  5373  axprlem2  5374  axprlem4  5376  axpr  5377  axprlem3OLD  5378  axprlem4OLD  5379  axprlem5OLD  5380  axprOLD  5381  exel  5388  rext  5403  exss  5418  snopeqop  5461  propssopi  5463  uniopel  5471  opthhausdorff  5472  opthhausdorff0  5473  wefrc  5625  relopabi  5776  relop  5804  dmrnssfld  5926  iss  5995  sofld  6148  ordun  6426  funimass2  6583  fvbr0  6869  fvmptg  6948  funsndifnop  7105  ov3  7532  elovmpo  7614  dford5  7740  limsssuc  7806  tfisi  7815  finds1  7855  frxp  8082  frxp2  8100  frxp3  8107  dfrecs3  8318  tfrlem1  8321  oaordi  8487  oaword2  8494  omeulem1  8523  oeworde  8534  oelim2  8536  nnaordi  8559  oaabs2  8590  limenpsi  9093  dif1en  9101  dif1enOLD  9103  enp1iOLD  9201  ordunifi  9213  fidomdm  9261  dffi3  9358  oismo  9469  wdom2d  9509  wdomima2g  9515  epnsym  9538  suc11reg  9548  elom3  9577  cantnfval2  9598  rankunb  9779  rankval4  9796  karden  9824  cardsn  9898  cardlim  9901  cardprclem  9908  fseqdom  9955  dfac12lem3  10075  kmlem2  10081  kmlem10  10089  cflim2  10192  cfslb2n  10197  fin23lem27  10257  fin23lem17  10267  axcc3  10367  axcc4  10368  acncc  10369  domtriomlem  10371  axdclem2  10449  imadomg  10463  alephval2  10501  alephreg  10511  axextnd  10520  fpwwe2lem9  10568  pwfseq  10593  gch2  10604  axgroth3  10760  inaprc  10765  nlt1pi  10835  indpi  10836  1re  11150  mul02lem2  11327  addrid  11330  fimaxre  12103  fiminre  12106  supaddc  12126  supmul1  12128  rimul  12153  nnge1  12190  zneo  12593  ltweuz  13902  hashrabsn1  14315  hashf1lem2  14397  hash2pwpr  14417  climuni  15494  fsum2d  15713  fsumabs  15743  fsumrlim  15753  fsumo1  15754  fsumiun  15763  fprod2d  15923  efne0d  16039  efne0OLD  16041  ruclem13  16186  dvdslelem  16255  mod2eq1n2dvds  16293  nn0o1gt2  16327  divalglem0  16339  lcmfnnval  16570  prmreclem2  16864  prmreclem3  16865  mreexexd  17589  coaval  18010  xpcco  18124  pltirr  18274  frgpnabllem1  19787  ablfac1eulem  19988  prmgrpsimpgd  20030  mdetunilem9  22540  mretopd  23012  fiuncmp  23324  ptcmpfi  23733  filtop  23775  supnfcls  23940  flimfnfcls  23948  alexsubALTlem2  23968  alexsubALTlem4  23970  trust  24150  rectbntr0  24754  fsumcn  24794  ovoliunlem3  25438  ovolicc2lem4  25454  dyadmax  25532  vitali  25547  itgfsum  25761  dvmptfsum  25912  fta1g  26108  fta1  26249  aannenlem1  26269  aalioulem3  26275  logltb  26542  logdmn0  26582  ang180lem2  26753  angpined  26773  mumullem2  27123  lgsqrmodndvds  27297  gausslemma2dlem0i  27308  2lgs  27351  dchrisum0re  27457  chpdifbnd  27499  pntrlog2bnd  27528  pntibndlem3  27536  pnt3  27556  nofv  27602  nomaxmo  27643  nominmo  27644  noprc  27725  madebday  27849  addsproplem7  27922  negsproplem7  27980  elons2  28199  nbgrval  29316  vtxdginducedm1fi  29525  upgrewlkle2  29587  hiidge0  31077  chsupval  31314  chsupcl  31319  chsupss  31321  ococin  31387  chsupval2  31389  ssjo  31426  h1de2i  31532  pjss2i  31659  pjssmii  31660  sto2i  32216  stge1i  32217  stle0i  32218  stlei  32219  stlesi  32220  stm1i  32222  staddi  32225  stadd3i  32227  golem1  32250  stcltrlem1  32255  mdexchi  32314  chirred  32374  atabsi  32380  abrexdomjm  32486  iocinif  32754  cycpmcl  33088  elrgspnsubrunlem2  33215  voliune  34212  volfiniune  34213  probdif  34404  bnj849  34908  onvf1odlem4  35086  onvf1od  35087  kur14lem9  35194  gonarlem  35374  gonar  35375  goalrlem  35376  goalr  35377  sscoid  35894  limsucncmpi  36426  bj-axc10  36764  bj-alequex  36765  bj-spimtv  36775  bj-moeub  36830  bj-exlimvmpi  36892  bj-exlimmpi  36893  bj-restpw  37073  bj-isrvec  37275  finxpreclem4  37375  domalom  37385  wl-isseteq  37486  wl-embant  37491  wl-orel12  37492  wl-euequf  37555  poimirlem9  37616  abrexdom  37717  heiborlem10  37807  dvrunz  37941  iss2  38319  equcomi1  38886  ax12eq  38927  ax12el  38928  ax12inda  38934  ax12v2-o  38935  cvrnrefN  39268  pmod1i  39835  pmodN  39837  osumcllem11N  39953  pexmidlem8N  39964  pl42lem3N  39968  cdleme18b  40279  dochexmidlem8  41454  imadomfi  41983  sticksstones3  42129  sn-axprlem3  42198  sn-exelALT  42199  sn-1ne2  42246  remul02  42386  sn-0tie0  42432  pellexlem3  42812  pell1234qrne0  42834  hbtlem6  43111  onsucelab  43245  omabs2  43314  nadd2rabex  43368  or3or  44005  isotone1  44030  isotone2  44031  clsf2  44108  ismnushort  44283  radcnvrat  44296  3impexpbicom  44463  sb5ALT  44508  eexinst01  44509  ax6e2eq  44540  sineq0ALT  44919  tcfr  44946  ssclaxsep  44965  omssaxinf2  44971  nregmodel  45000  fzisoeu  45291  ovnsubaddlem2  46562  ormklocald  46865  natlocalincr  46867  tworepnotupword  46877  tannpoly  46884  funressnfv  47037  faovcl  47194  sprsymrelfo  47491  clnbgrval  47816  gpgedgiov  48049  gpgedg2ov  48050  gpgedg2iv  48051  pgnioedg1  48091  pgnioedg2  48092  pgnioedg3  48093  pgnioedg4  48094  pgnioedg5  48095  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  pgnbgreunbgrlem2lem3  48099  pgnbgreunbgrlem5lem1  48103  pgnbgreunbgrlem5lem2  48104  cznnring  48243  zlmodzxznm  48479  elbigolo1  48539  dignn0flhalflem1  48597  nn0sumshdig  48605  rrx2xpref1o  48700  fonex  48848  vsetrec  49685