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  714  mp3an3  1413  merco2  1661  equs4v  1930  equcomiv  1941  equcomi  1944  equvinv  1959  equviniva  1960  equvinivOLD  1961  aeveq  1982  aevOLD  2162  spimt  2253  equs4  2290  axc15  2303  ax12v2OLD  2342  2ax6elem  2449  pm13.183  3344  sbcth  3450  sbcth2  3523  ssun3  3778  ssun4  3779  uneqdifeqOLD  4058  ralf0OLD  4079  elpreqprlem  4395  uniintsn  4514  rext  4916  exss  4931  propssopi  4971  uniopel  4978  wefrc  5108  relopabi  5245  relop  5272  dmrnssfld  5384  iss  5447  sofld  5581  ordun  5829  nfunv  5921  funimass2  5972  fvbr0  6215  fvmptg  6280  funsndifnop  6416  fovcl  6765  ov3  6797  elovmpt2  6879  limsssuc  7050  tfisi  7058  finds1  7095  frxp  7287  wfrlem5  7419  wfrlem16  7430  dfrecs3  7469  tfrlem1  7472  oaordi  7626  oaword2  7633  omeulem1  7662  oeworde  7673  oelim2  7675  nnaordi  7698  oaabs2  7725  0domg  8087  limenpsi  8135  enp1i  8195  findcard2  8200  ordunifi  8210  fidomdm  8243  dffi3  8337  oismo  8445  wdom2d  8485  wdomima2g  8491  suc11reg  8516  elom3  8545  cantnfval2  8566  rankunb  8713  rankval4  8730  karden  8758  cardsn  8795  cardlim  8798  cardprclem  8805  fseqdom  8849  dfac12lem3  8967  kmlem2  8973  kmlem10  8981  cflim2  9085  cfslb2n  9090  fin23lem27  9150  axcc3  9260  axcc4  9261  acncc  9262  domtriomlem  9264  axdclem2  9342  imadomg  9356  alephval2  9394  alephreg  9404  axextnd  9413  fpwwe2lem10  9461  pwfseq  9486  gch2  9497  axgroth3  9653  inaprc  9658  nlt1pi  9728  indpi  9729  1re  10039  mul02lem2  10213  addid1  10216  fimaxre  10968  supaddc  10990  supmul1  10992  inelr  11010  rimul  11011  nnge1  11046  zneo  11460  ltweuz  12760  hashrabsn1  13163  hashf1lem2  13240  hash2pwpr  13258  climuni  14283  fsum2d  14502  fsumabs  14533  fsumrlim  14543  fsumo1  14544  fsumiun  14553  fprod2d  14711  efne0  14827  ruclem13  14971  dvdslelem  15031  mod2eq1n2dvds  15071  nn0o1gt2  15097  divalglem0  15116  lcmfnnval  15337  prmreclem2  15621  prmreclem3  15622  mreexexd  16308  mreexexdOLD  16309  coaval  16718  xpcco  16823  pltirr  16963  frgpnabllem1  18276  ablfac1eulem  18471  mdetunilem9  20426  mretopd  20896  fiuncmp  21207  ptcmpfi  21616  filtop  21659  supnfcls  21824  flimfnfcls  21832  alexsubALTlem2  21852  alexsubALTlem4  21854  trust  22033  rectbntr0  22635  fsumcn  22673  ovoliunlem3  23272  ovolicc2lem4  23288  dyadmax  23366  vitali  23382  itgfsum  23593  dvmptfsum  23738  fta1g  23927  fta1  24063  aannenlem1  24083  aalioulem3  24089  logltb  24346  logdmn0  24386  ang180lem2  24540  angpined  24557  mumullem2  24906  lgsqrmodndvds  25078  gausslemma2dlem0i  25089  2lgs  25132  dchrisum0re  25202  chpdifbnd  25244  pntrlog2bnd  25273  pntibndlem3  25281  pnt3  25301  nbgrval  26234  vtxdginducedm1fi  26440  upgrewlkle2  26502  hiidge0  27955  chsupval  28194  chsupcl  28199  chsupss  28201  ococin  28267  chsupval2  28269  ssjo  28306  h1de2i  28412  pjss2i  28539  pjssmii  28540  sto2i  29096  stge1i  29097  stle0i  29098  stlei  29099  stlesi  29100  stm1i  29102  staddi  29105  stadd3i  29107  golem1  29130  stcltrlem1  29135  mdexchi  29194  chirred  29254  atabsi  29260  rmoeqALT  29327  abrexdomjm  29345  iocinif  29543  voliune  30292  volfiniune  30293  probdif  30482  bnj849  30995  kur14lem9  31196  dford5  31608  frrlem5  31784  nofv  31810  nomaxmo  31847  noprc  31895  sscoid  32020  limsucncmpi  32444  bj-peirce  32543  bj-sbex  32626  bj-alequexv  32655  bj-axc10  32707  bj-alequex  32708  bj-spimtv  32718  bj-exlimmpi  32905  bj-restpw  33045  finxpreclem4  33231  wl-embant  33293  wl-orel12  33294  wl-euequ1f  33356  poimirlem9  33418  abrexdom  33525  heiborlem10  33619  dvrunz  33753  iss2  34112  equcomi1  34185  ax12eq  34226  ax12el  34227  ax12inda  34233  ax12v2-o  34234  cvrnrefN  34569  pmod1i  35134  pmodN  35136  osumcllem11N  35252  pexmidlem8N  35263  pl42lem3N  35267  cdleme18b  35579  dochexmidlem8  36756  pellexlem3  37395  pell1234qrne0  37417  hbtlem6  37699  or3or  38319  isotone1  38346  isotone2  38347  clsf2  38424  radcnvrat  38513  3impexpbicom  38685  sb5ALT  38731  eexinst01  38732  ax6e2eq  38773  sineq0ALT  39173  fzisoeu  39514  ovnsubaddlem2  40785  funressnfv  41208  faovcl  41280  sprsymrelfo  41747  cznnring  41956  zlmodzxznm  42286  elbigolo1  42351  dignn0flhalflem1  42409  nn0sumshdig  42417  vsetrec  42446