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  3757  sbcth2  3836  ssun3  4131  ssun4  4132  elpreqprlem  4817  uniintsn  4935  sepexlem  5238  axprlem1  5362  axprlem2  5363  axprlem4  5365  axpr  5366  axprlem3OLD  5367  axprlem4OLD  5368  axprlem5OLD  5369  axprOLD  5370  exel  5377  rext  5391  exss  5406  snopeqop  5449  propssopi  5451  uniopel  5459  opthhausdorff  5460  opthhausdorff0  5461  wefrc  5613  relopabi  5765  relop  5793  dmrnssfld  5915  iss  5986  sofld  6136  ordun  6413  funimass2  6565  fvbr0  6849  fvmptg  6928  funsndifnop  7085  ov3  7512  elovmpo  7594  dford5  7720  limsssuc  7783  tfisi  7792  finds1  7832  frxp  8059  frxp2  8077  frxp3  8084  dfrecs3  8295  tfrlem1  8298  oaordi  8464  oaword2  8471  omeulem1  8500  oeworde  8511  oelim2  8513  nnaordi  8536  oaabs2  8567  limenpsi  9069  dif1en  9075  ordunifi  9179  fidomdm  9224  dffi3  9321  oismo  9432  wdom2d  9472  wdomima2g  9478  epnsym  9505  suc11reg  9515  elom3  9544  cantnfval2  9565  rankunb  9746  rankval4  9763  karden  9791  cardsn  9865  cardlim  9868  cardprclem  9875  fseqdom  9920  dfac12lem3  10040  kmlem2  10046  kmlem10  10054  cflim2  10157  cfslb2n  10162  fin23lem27  10222  fin23lem17  10232  axcc3  10332  axcc4  10333  acncc  10334  domtriomlem  10336  axdclem2  10414  imadomg  10428  alephval2  10466  alephreg  10476  axextnd  10485  fpwwe2lem9  10533  pwfseq  10558  gch2  10569  axgroth3  10725  inaprc  10730  nlt1pi  10800  indpi  10801  1re  11115  mul02lem2  11293  addrid  11296  fimaxre  12069  fiminre  12072  supaddc  12092  supmul1  12094  rimul  12119  nnge1  12156  zneo  12559  ltweuz  13868  hashrabsn1  14281  hashf1lem2  14363  hash2pwpr  14383  climuni  15459  fsum2d  15678  fsumabs  15708  fsumrlim  15718  fsumo1  15719  fsumiun  15728  fprod2d  15888  efne0d  16004  efne0OLD  16006  ruclem13  16151  dvdslelem  16220  mod2eq1n2dvds  16258  nn0o1gt2  16292  divalglem0  16304  lcmfnnval  16535  prmreclem2  16829  prmreclem3  16830  mreexexd  17554  coaval  17975  xpcco  18089  pltirr  18239  frgpnabllem1  19752  ablfac1eulem  19953  prmgrpsimpgd  19995  mdetunilem9  22505  mretopd  22977  fiuncmp  23289  ptcmpfi  23698  filtop  23740  supnfcls  23905  flimfnfcls  23913  alexsubALTlem2  23933  alexsubALTlem4  23935  trust  24115  rectbntr0  24719  fsumcn  24759  ovoliunlem3  25403  ovolicc2lem4  25419  dyadmax  25497  vitali  25512  itgfsum  25726  dvmptfsum  25877  fta1g  26073  fta1  26214  aannenlem1  26234  aalioulem3  26240  logltb  26507  logdmn0  26547  ang180lem2  26718  angpined  26738  mumullem2  27088  lgsqrmodndvds  27262  gausslemma2dlem0i  27273  2lgs  27316  dchrisum0re  27422  chpdifbnd  27464  pntrlog2bnd  27493  pntibndlem3  27501  pnt3  27521  nofv  27567  nomaxmo  27608  nominmo  27609  noprc  27690  madebday  27814  addsproplem7  27887  negsproplem7  27945  elons2  28164  nbgrval  29281  vtxdginducedm1fi  29490  upgrewlkle2  29552  hiidge0  31042  chsupval  31279  chsupcl  31284  chsupss  31286  ococin  31352  chsupval2  31354  ssjo  31391  h1de2i  31497  pjss2i  31624  pjssmii  31625  sto2i  32181  stge1i  32182  stle0i  32183  stlei  32184  stlesi  32185  stm1i  32187  staddi  32190  stadd3i  32192  golem1  32215  stcltrlem1  32220  mdexchi  32279  chirred  32339  atabsi  32345  abrexdomjm  32451  iocinif  32725  cycpmcl  33059  elrgspnsubrunlem2  33189  voliune  34202  volfiniune  34203  probdif  34394  bnj849  34898  onvf1odlem4  35089  onvf1od  35090  kur14lem9  35197  gonarlem  35377  gonar  35378  goalrlem  35379  goalr  35380  sscoid  35897  limsucncmpi  36429  bj-axc10  36767  bj-alequex  36768  bj-spimtv  36778  bj-moeub  36833  bj-exlimvmpi  36895  bj-exlimmpi  36896  bj-restpw  37076  bj-isrvec  37278  finxpreclem4  37378  domalom  37388  wl-isseteq  37489  wl-embant  37494  wl-orel12  37495  wl-euequf  37558  poimirlem9  37619  abrexdom  37720  heiborlem10  37810  dvrunz  37944  iss2  38322  equcomi1  38889  ax12eq  38930  ax12el  38931  ax12inda  38937  ax12v2-o  38938  cvrnrefN  39271  pmod1i  39837  pmodN  39839  osumcllem11N  39955  pexmidlem8N  39966  pl42lem3N  39970  cdleme18b  40281  dochexmidlem8  41456  imadomfi  41985  sticksstones3  42131  sn-axprlem3  42200  sn-exelALT  42201  sn-1ne2  42248  remul02  42388  sn-0tie0  42434  pellexlem3  42814  pell1234qrne0  42836  hbtlem6  43112  onsucelab  43246  omabs2  43315  nadd2rabex  43369  or3or  44006  isotone1  44031  isotone2  44032  clsf2  44109  ismnushort  44284  radcnvrat  44297  3impexpbicom  44464  sb5ALT  44509  eexinst01  44510  ax6e2eq  44541  sineq0ALT  44920  tcfr  44947  ssclaxsep  44966  omssaxinf2  44972  nregmodel  45001  fzisoeu  45292  ovnsubaddlem2  46562  ormklocald  46865  natlocalincr  46867  tworepnotupword  46877  tannpoly  46884  funressnfv  47037  faovcl  47194  sprsymrelfo  47491  clnbgrval  47816  gpgedgiov  48059  gpgedg2ov  48060  gpgedg2iv  48061  pgnioedg1  48102  pgnioedg2  48103  pgnioedg3  48104  pgnioedg4  48105  pgnioedg5  48106  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  cznnring  48256  zlmodzxznm  48492  elbigolo1  48552  dignn0flhalflem1  48610  nn0sumshdig  48618  rrx2xpref1o  48713  fonex  48861  vsetrec  49698