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  1737  equs4v  2001  alequexv  2002  equcomiv  2015  equcomi  2018  equvinva  2031  aeveq  2059  spimt  2388  equs4  2418  axc15  2424  2ax6elem  2472  dfeumo  2534  mo4  2564  sbcth  3753  sbcth2  3832  ssun3  4130  ssun4  4131  elpreqprlem  4820  uniintsn  4938  sepexlem  5242  axprlem1  5366  axprlem2  5367  axprlem4  5369  axpr  5370  axprlem3OLD  5371  axprlem4OLD  5372  axprlem5OLD  5373  axprOLD  5374  exel  5381  rext  5394  exss  5409  snopeqop  5452  propssopi  5454  uniopel  5462  opthhausdorff  5463  opthhausdorff0  5464  wefrc  5616  relopabi  5769  relop  5797  dmrnssfld  5921  iss  5992  sofld  6143  ordun  6421  funimass2  6573  fvbr0  6859  fvmptg  6937  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  9078  dif1en  9084  ordunifi  9188  fidomdm  9232  dffi3  9332  oismo  9443  wdom2d  9483  wdomima2g  9489  epnsym  9516  suc11reg  9526  elom3  9555  cantnfval2  9576  rankunb  9760  rankval4  9777  karden  9805  cardsn  9879  cardlim  9882  cardprclem  9889  fseqdom  9934  dfac12lem3  10054  kmlem2  10060  kmlem10  10068  cflim2  10171  cfslb2n  10176  fin23lem27  10236  fin23lem17  10246  axcc3  10346  axcc4  10347  acncc  10348  domtriomlem  10350  axdclem2  10428  imadomg  10442  alephval2  10481  alephreg  10491  axextnd  10500  fpwwe2lem9  10548  pwfseq  10573  gch2  10584  axgroth3  10740  inaprc  10745  nlt1pi  10815  indpi  10816  1re  11130  mul02lem2  11308  addrid  11311  fimaxre  12084  fiminre  12087  supaddc  12107  supmul1  12109  rimul  12134  nnge1  12171  zneo  12573  ltweuz  13882  hashrabsn1  14295  hashf1lem2  14377  hash2pwpr  14397  climuni  15473  fsum2d  15692  fsumabs  15722  fsumrlim  15732  fsumo1  15733  fsumiun  15742  fprod2d  15902  efne0d  16018  efne0OLD  16020  ruclem13  16165  dvdslelem  16234  mod2eq1n2dvds  16272  nn0o1gt2  16306  divalglem0  16318  lcmfnnval  16549  prmreclem2  16843  prmreclem3  16844  mreexexd  17569  coaval  17990  xpcco  18104  pltirr  18254  frgpnabllem1  19800  ablfac1eulem  20001  prmgrpsimpgd  20043  mdetunilem9  22562  mretopd  23034  fiuncmp  23346  ptcmpfi  23755  filtop  23797  supnfcls  23962  flimfnfcls  23970  alexsubALTlem2  23990  alexsubALTlem4  23992  trust  24171  rectbntr0  24775  fsumcn  24815  ovoliunlem3  25459  ovolicc2lem4  25475  dyadmax  25553  vitali  25568  itgfsum  25782  dvmptfsum  25933  fta1g  26129  fta1  26270  aannenlem1  26290  aalioulem3  26296  logltb  26563  logdmn0  26603  ang180lem2  26774  angpined  26794  mumullem2  27144  lgsqrmodndvds  27318  gausslemma2dlem0i  27329  2lgs  27372  dchrisum0re  27478  chpdifbnd  27520  pntrlog2bnd  27549  pntibndlem3  27557  pnt3  27577  nofv  27623  nomaxmo  27664  nominmo  27665  noprc  27746  madebday  27872  addsproplem7  27945  negsproplem7  28003  elons2  28226  nbgrval  29358  vtxdginducedm1fi  29567  upgrewlkle2  29629  hiidge0  31122  chsupval  31359  chsupcl  31364  chsupss  31366  ococin  31432  chsupval2  31434  ssjo  31471  h1de2i  31577  pjss2i  31704  pjssmii  31705  sto2i  32261  stge1i  32262  stle0i  32263  stlei  32264  stlesi  32265  stm1i  32267  staddi  32270  stadd3i  32272  golem1  32295  stcltrlem1  32300  mdexchi  32359  chirred  32419  atabsi  32425  abrexdomjm  32531  iocinif  32810  cycpmcl  33147  elrgspnsubrunlem2  33279  voliune  34335  volfiniune  34336  probdif  34526  bnj849  35030  onvf1odlem4  35249  onvf1od  35250  kur14lem9  35357  gonarlem  35537  gonar  35538  goalrlem  35539  goalr  35540  sscoid  36054  limsucncmpi  36588  bj-axc10  36927  bj-alequex  36928  bj-spimtv  36938  bj-moeub  36993  bj-exlimvmpi  37055  bj-exlimmpi  37056  bj-restpw  37236  bj-isrvec  37438  finxpreclem4  37538  domalom  37548  wl-isseteq  37649  wl-embant  37654  wl-orel12  37655  wl-euequf  37718  poimirlem9  37769  abrexdom  37870  heiborlem10  37960  dvrunz  38094  iss2  38476  equcomi1  39099  ax12eq  39140  ax12el  39141  ax12inda  39147  ax12v2-o  39148  cvrnrefN  39481  pmod1i  40047  pmodN  40049  osumcllem11N  40165  pexmidlem8N  40176  pl42lem3N  40180  cdleme18b  40491  dochexmidlem8  41666  imadomfi  42195  sticksstones3  42341  sn-axprlem3  42415  sn-exelALT  42416  sn-1ne2  42462  remul02  42602  sn-0tie0  42648  pellexlem3  43015  pell1234qrne0  43037  hbtlem6  43313  onsucelab  43447  omabs2  43516  nadd2rabex  43570  or3or  44206  isotone1  44231  isotone2  44232  clsf2  44309  ismnushort  44484  radcnvrat  44497  3impexpbicom  44663  sb5ALT  44708  eexinst01  44709  ax6e2eq  44740  sineq0ALT  45119  tcfr  45146  ssclaxsep  45165  omssaxinf2  45171  nregmodel  45200  fzisoeu  45490  ovnsubaddlem2  46757  ormklocald  47060  natlocalincr  47062  tannpoly  47078  funressnfv  47231  faovcl  47388  sprsymrelfo  47685  clnbgrval  48010  gpgedgiov  48253  gpgedg2ov  48254  gpgedg2iv  48255  pgnioedg1  48296  pgnioedg2  48297  pgnioedg3  48298  pgnioedg4  48299  pgnioedg5  48300  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgnbgreunbgrlem2lem3  48304  pgnbgreunbgrlem5lem1  48308  pgnbgreunbgrlem5lem2  48309  cznnring  48450  zlmodzxznm  48685  elbigolo1  48745  dignn0flhalflem1  48803  nn0sumshdig  48811  rrx2xpref1o  48906  fonex  49054  vsetrec  49890