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  1449  merco2  1733  equs4v  1997  alequexv  1998  equcomiv  2011  equcomi  2014  equvinva  2027  aeveq  2054  spimt  2389  equs4  2419  axc15  2425  2ax6elem  2473  dfeumo  2535  mo4  2564  sbcth  3806  sbcth2  3893  ssun3  4190  ssun4  4191  elpreqprlem  4871  uniintsn  4990  sepexlem  5305  axprlem1  5429  axprlem2  5430  axprlem4  5432  axpr  5433  axprlem3OLD  5434  axprlem4OLD  5435  axprlem5OLD  5436  axprOLD  5437  exel  5444  rext  5459  exss  5474  snopeqop  5516  propssopi  5518  uniopel  5526  opthhausdorff  5527  opthhausdorff0  5528  wefrc  5683  relopabi  5835  relop  5864  dmrnssfld  5987  iss  6055  sofld  6209  ordun  6490  funimass2  6651  fvbr0  6936  fvmptg  7014  funsndifnop  7171  ov3  7596  elovmpo  7678  dford5  7803  limsssuc  7871  tfisi  7880  finds1  7922  frxp  8150  frxp2  8168  frxp3  8175  wfrlem5OLD  8352  wfrlem16OLD  8363  dfrecs3  8411  dfrecs3OLD  8412  tfrlem1  8415  oaordi  8583  oaword2  8590  omeulem1  8619  oeworde  8630  oelim2  8632  nnaordi  8655  oaabs2  8686  0domgOLD  9140  limenpsi  9191  dif1en  9199  dif1enOLD  9201  enp1iOLD  9312  ordunifi  9324  fidomdm  9372  dffi3  9469  oismo  9578  wdom2d  9618  wdomima2g  9624  epnsym  9647  suc11reg  9657  elom3  9686  cantnfval2  9707  rankunb  9888  rankval4  9905  karden  9933  cardsn  10007  cardlim  10010  cardprclem  10017  fseqdom  10064  dfac12lem3  10184  kmlem2  10190  kmlem10  10198  cflim2  10301  cfslb2n  10306  fin23lem27  10366  fin23lem17  10376  axcc3  10476  axcc4  10477  acncc  10478  domtriomlem  10480  axdclem2  10558  imadomg  10572  alephval2  10610  alephreg  10620  axextnd  10629  fpwwe2lem9  10677  pwfseq  10702  gch2  10713  axgroth3  10869  inaprc  10874  nlt1pi  10944  indpi  10945  1re  11259  mul02lem2  11436  addrid  11439  fimaxre  12210  fiminre  12213  supaddc  12233  supmul1  12235  inelr  12254  rimul  12255  nnge1  12292  zneo  12699  ltweuz  13999  hashrabsn1  14410  hashf1lem2  14492  hash2pwpr  14512  climuni  15585  fsum2d  15804  fsumabs  15834  fsumrlim  15844  fsumo1  15845  fsumiun  15854  fprod2d  16014  efne0  16130  ruclem13  16275  dvdslelem  16343  mod2eq1n2dvds  16381  nn0o1gt2  16415  divalglem0  16427  lcmfnnval  16658  prmreclem2  16951  prmreclem3  16952  mreexexd  17693  coaval  18122  xpcco  18239  pltirr  18393  frgpnabllem1  19906  ablfac1eulem  20107  prmgrpsimpgd  20149  mdetunilem9  22642  mretopd  23116  fiuncmp  23428  ptcmpfi  23837  filtop  23879  supnfcls  24044  flimfnfcls  24052  alexsubALTlem2  24072  alexsubALTlem4  24074  trust  24254  rectbntr0  24868  fsumcn  24908  ovoliunlem3  25553  ovolicc2lem4  25569  dyadmax  25647  vitali  25662  itgfsum  25877  dvmptfsum  26028  fta1g  26224  fta1  26365  aannenlem1  26385  aalioulem3  26391  logltb  26657  logdmn0  26697  ang180lem2  26868  angpined  26888  mumullem2  27238  lgsqrmodndvds  27412  gausslemma2dlem0i  27423  2lgs  27466  dchrisum0re  27572  chpdifbnd  27614  pntrlog2bnd  27643  pntibndlem3  27651  pnt3  27671  nofv  27717  nomaxmo  27758  nominmo  27759  noprc  27839  madebday  27953  addsproplem7  28023  negsproplem7  28081  elons2  28296  nbgrval  29368  vtxdginducedm1fi  29577  upgrewlkle2  29639  hiidge0  31127  chsupval  31364  chsupcl  31369  chsupss  31371  ococin  31437  chsupval2  31439  ssjo  31476  h1de2i  31582  pjss2i  31709  pjssmii  31710  sto2i  32266  stge1i  32267  stle0i  32268  stlei  32269  stlesi  32270  stm1i  32272  staddi  32275  stadd3i  32277  golem1  32300  stcltrlem1  32305  mdexchi  32364  chirred  32424  atabsi  32430  abrexdomjm  32535  iocinif  32790  cycpmcl  33119  voliune  34210  volfiniune  34211  probdif  34402  bnj849  34918  kur14lem9  35199  gonarlem  35379  gonar  35380  goalrlem  35381  goalr  35382  sscoid  35895  limsucncmpi  36428  bj-axc10  36766  bj-alequex  36767  bj-spimtv  36777  bj-moeub  36832  bj-exlimvmpi  36894  bj-exlimmpi  36895  bj-restpw  37075  bj-isrvec  37277  finxpreclem4  37377  domalom  37387  wl-isseteq  37486  wl-embant  37491  wl-orel12  37492  wl-euequf  37555  poimirlem9  37616  abrexdom  37717  heiborlem10  37807  dvrunz  37941  iss2  38326  equcomi1  38882  ax12eq  38923  ax12el  38924  ax12inda  38930  ax12v2-o  38931  cvrnrefN  39264  pmod1i  39831  pmodN  39833  osumcllem11N  39949  pexmidlem8N  39960  pl42lem3N  39964  cdleme18b  40275  dochexmidlem8  41450  imadomfi  41984  sticksstones3  42130  sn-axprlem3  42235  sn-exelALT  42236  sn-1ne2  42279  efne0d  42352  remul02  42412  sn-0tie0  42446  pellexlem3  42819  pell1234qrne0  42841  hbtlem6  43118  onsucelab  43253  omabs2  43322  nadd2rabex  43376  or3or  44013  isotone1  44038  isotone2  44039  clsf2  44116  ismnushort  44297  radcnvrat  44310  3impexpbicom  44477  sb5ALT  44523  eexinst01  44524  ax6e2eq  44555  sineq0ALT  44935  ssclaxsep  44947  fzisoeu  45251  ovnsubaddlem2  46527  natlocalincr  46830  tworepnotupword  46840  funressnfv  46993  faovcl  47150  sprsymrelfo  47422  clnbgrval  47747  cznnring  48106  zlmodzxznm  48343  elbigolo1  48407  dignn0flhalflem1  48465  nn0sumshdig  48473  rrx2xpref1o  48568  vsetrec  48934