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  2390  equs4  2420  axc15  2426  2ax6elem  2474  dfeumo  2536  mo4  2566  sbcth  3755  sbcth2  3834  ssun3  4132  ssun4  4133  elpreqprlem  4822  uniintsn  4940  sepexlem  5244  axprlem1  5368  axprlem2  5369  axprlem4  5371  axpr  5372  axprlem3OLD  5373  axprlem4OLD  5374  axprlem5OLD  5375  axprOLD  5376  exel  5383  rext  5396  exss  5411  snopeqop  5454  propssopi  5456  uniopel  5464  opthhausdorff  5465  opthhausdorff0  5466  wefrc  5618  relopabi  5771  relop  5799  dmrnssfld  5923  iss  5994  sofld  6145  ordun  6423  funimass2  6575  fvbr0  6861  fvmptg  6939  funsndifnop  7096  ov3  7521  elovmpo  7603  dford5  7729  limsssuc  7792  tfisi  7801  finds1  7841  frxp  8068  frxp2  8086  frxp3  8093  dfrecs3  8304  tfrlem1  8307  oaordi  8473  oaword2  8480  omeulem1  8509  oeworde  8521  oelim2  8523  nnaordi  8546  oaabs2  8577  limenpsi  9082  dif1en  9088  ordunifi  9192  fidomdm  9236  dffi3  9336  oismo  9447  wdom2d  9487  wdomima2g  9493  epnsym  9520  suc11reg  9530  elom3  9559  cantnfval2  9580  rankunb  9764  rankval4  9781  karden  9809  cardsn  9883  cardlim  9886  cardprclem  9893  fseqdom  9938  dfac12lem3  10058  kmlem2  10064  kmlem10  10072  cflim2  10175  cfslb2n  10180  fin23lem27  10240  fin23lem17  10250  axcc3  10350  axcc4  10351  acncc  10352  domtriomlem  10354  axdclem2  10432  imadomg  10446  alephval2  10485  alephreg  10495  axextnd  10504  fpwwe2lem9  10552  pwfseq  10577  gch2  10588  axgroth3  10744  inaprc  10749  nlt1pi  10819  indpi  10820  1re  11134  mul02lem2  11312  addrid  11315  fimaxre  12088  fiminre  12091  supaddc  12111  supmul1  12113  rimul  12138  nnge1  12175  zneo  12577  ltweuz  13886  hashrabsn1  14299  hashf1lem2  14381  hash2pwpr  14401  climuni  15477  fsum2d  15696  fsumabs  15726  fsumrlim  15736  fsumo1  15737  fsumiun  15746  fprod2d  15906  efne0d  16022  efne0OLD  16024  ruclem13  16169  dvdslelem  16238  mod2eq1n2dvds  16276  nn0o1gt2  16310  divalglem0  16322  lcmfnnval  16553  prmreclem2  16847  prmreclem3  16848  mreexexd  17573  coaval  17994  xpcco  18108  pltirr  18258  frgpnabllem1  19804  ablfac1eulem  20005  prmgrpsimpgd  20047  mdetunilem9  22566  mretopd  23038  fiuncmp  23350  ptcmpfi  23759  filtop  23801  supnfcls  23966  flimfnfcls  23974  alexsubALTlem2  23994  alexsubALTlem4  23996  trust  24175  rectbntr0  24779  fsumcn  24819  ovoliunlem3  25463  ovolicc2lem4  25479  dyadmax  25557  vitali  25572  itgfsum  25786  dvmptfsum  25937  fta1g  26133  fta1  26274  aannenlem1  26294  aalioulem3  26300  logltb  26567  logdmn0  26607  ang180lem2  26778  angpined  26798  mumullem2  27148  lgsqrmodndvds  27322  gausslemma2dlem0i  27333  2lgs  27376  dchrisum0re  27482  chpdifbnd  27524  pntrlog2bnd  27553  pntibndlem3  27561  pnt3  27581  nofv  27627  nomaxmo  27668  nominmo  27669  noprc  27754  madebday  27898  addsproplem7  27973  negsproplem7  28032  elons2  28256  nbgrval  29411  vtxdginducedm1fi  29620  upgrewlkle2  29682  hiidge0  31175  chsupval  31412  chsupcl  31417  chsupss  31419  ococin  31485  chsupval2  31487  ssjo  31524  h1de2i  31630  pjss2i  31757  pjssmii  31758  sto2i  32314  stge1i  32315  stle0i  32316  stlei  32317  stlesi  32318  stm1i  32320  staddi  32323  stadd3i  32325  golem1  32348  stcltrlem1  32353  mdexchi  32412  chirred  32472  atabsi  32478  abrexdomjm  32584  iocinif  32863  cycpmcl  33200  elrgspnsubrunlem2  33332  voliune  34388  volfiniune  34389  probdif  34579  bnj849  35083  onvf1odlem4  35302  onvf1od  35303  kur14lem9  35410  gonarlem  35590  gonar  35591  goalrlem  35592  goalr  35593  sscoid  36107  limsucncmpi  36641  bj-axc10  36986  bj-alequex  36987  bj-spimtv  36997  bj-moeub  37052  bj-exlimvmpi  37114  bj-exlimmpi  37115  bj-restpw  37299  bj-isrvec  37501  finxpreclem4  37601  domalom  37611  wl-isseteq  37712  wl-embant  37717  wl-orel12  37718  wl-euequf  37781  poimirlem9  37832  abrexdom  37933  heiborlem10  38023  dvrunz  38157  iss2  38542  equcomi1  39182  ax12eq  39223  ax12el  39224  ax12inda  39230  ax12v2-o  39231  cvrnrefN  39564  pmod1i  40130  pmodN  40132  osumcllem11N  40248  pexmidlem8N  40259  pl42lem3N  40263  cdleme18b  40574  dochexmidlem8  41749  imadomfi  42278  sticksstones3  42424  sn-axprlem3  42496  sn-exelALT  42497  sn-1ne2  42541  remul02  42681  sn-0tie0  42727  pellexlem3  43094  pell1234qrne0  43116  hbtlem6  43392  onsucelab  43526  omabs2  43595  nadd2rabex  43649  or3or  44285  isotone1  44310  isotone2  44311  clsf2  44388  ismnushort  44563  radcnvrat  44576  3impexpbicom  44742  sb5ALT  44787  eexinst01  44788  ax6e2eq  44819  sineq0ALT  45198  tcfr  45225  ssclaxsep  45244  omssaxinf2  45250  nregmodel  45279  fzisoeu  45569  ovnsubaddlem2  46836  ormklocald  47139  natlocalincr  47141  tannpoly  47157  funressnfv  47310  faovcl  47467  sprsymrelfo  47764  clnbgrval  48089  gpgedgiov  48332  gpgedg2ov  48333  gpgedg2iv  48334  pgnioedg1  48375  pgnioedg2  48376  pgnioedg3  48377  pgnioedg4  48378  pgnioedg5  48379  pgnbgreunbgrlem2lem1  48381  pgnbgreunbgrlem2lem2  48382  pgnbgreunbgrlem2lem3  48383  pgnbgreunbgrlem5lem1  48387  pgnbgreunbgrlem5lem2  48388  cznnring  48529  zlmodzxznm  48764  elbigolo1  48824  dignn0flhalflem1  48882  nn0sumshdig  48890  rrx2xpref1o  48985  fonex  49133  vsetrec  49969