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  708  mp3an3  1472  merco2  1757  equs4v  2021  alequexv  2022  equcomiv  2035  equcomi  2038  equvinva  2051  aeveq  2079  spimt  2418  equs4  2448  axc15  2454  2ax6elem  2502  dfeumo  2564  mo4  2594  sbcth  3760  sbcth2  3838  ssun3  4133  ssun4  4134  elpreqprlem  4825  uniintsn  4944  sepexlem  5250  axprlem2  5382  axprlem4  5384  axpr  5385  axprlem1OLD  5386  axprlem3OLD  5387  axprlem4OLD  5388  axprlem5OLD  5389  axprOLD  5390  axprglem  5394  exel  5402  rext  5416  exss  5431  snopeqop  5476  propssopi  5478  uniopel  5486  opthhausdorff  5487  opthhausdorff0  5488  wefrc  5642  relopabi  5796  relop  5823  dmrnssfld  5951  iss  6025  sofld  6174  ordun  6453  funimass2  6605  fvbr0  6895  fvmptg  6974  funsndifnop  7135  ov3  7560  elovmpo  7642  dford5  7768  limsssuc  7831  tfisi  7840  finds1  7881  frxp  8107  frxp2  8125  frxp3  8132  dfrecs3  8344  tfrlem1  8347  oaordi  8516  oaword2  8523  omeulem1  8552  oeworde  8564  oelim2  8566  nnaordi  8589  oaabs2  8620  limenpsi  9125  dif1en  9131  ordunifi  9235  fidomdm  9278  dffi3  9378  oismo  9489  wdom2d  9529  wdomima2g  9535  epnsym  9565  suc11reg  9575  elom3  9604  cantnfval2  9625  rankunb  9809  rankval4  9826  karden  9854  cardsn  9928  cardlim  9931  cardprclem  9938  fseqdom  9983  dfac12lem3  10103  kmlem2  10109  kmlem10  10117  cflim2  10221  cfslb2n  10226  fin23lem27  10286  fin23lem17  10296  axcc3  10396  axcc4  10397  acncc  10398  domtriomlem  10400  axdclem2  10478  imadomg  10492  alephval2  10531  alephreg  10541  axextnd  10550  fpwwe2lem9  10598  pwfseq  10623  gch2  10634  axgroth3  10790  inaprc  10795  nlt1pi  10865  indpi  10866  1re  11182  mul02lem2  11361  addrid  11364  fimaxre  12137  fiminre  12140  supaddc  12160  supmul1  12162  rimul  12187  nnge1  12242  zneo  12657  ltweuz  13975  hashrabsn1  14388  hashf1lem2  14470  hash2pwpr  14490  climuni  15580  fsum2d  15799  fsumabs  15830  fsumrlim  15840  fsumo1  15841  fsumiun  15850  fprod2d  16012  efne0d  16128  efne0OLD  16130  ruclem13  16275  dvdslelem  16344  mod2eq1n2dvds  16382  nn0o1gt2  16416  divalglem0  16428  lcmfnnval  16659  prmreclem2  16954  prmreclem3  16955  mreexexd  17681  coaval  18102  xpcco  18216  pltirr  18366  frgpnabllem1  19914  ablfac1eulem  20115  prmgrpsimpgd  20157  mdetunilem9  22681  mretopd  23153  fiuncmp  23465  ptcmpfi  23874  filtop  23916  supnfcls  24081  flimfnfcls  24089  alexsubALTlem2  24109  alexsubALTlem4  24111  trust  24290  rectbntr0  24894  fsumcn  24933  ovoliunlem3  25567  ovolicc2lem4  25583  dyadmax  25661  vitali  25676  itgfsum  25890  dvmptfsum  26038  fta1g  26231  fta1  26373  aannenlem1  26393  aalioulem3  26399  logltb  26666  logdmn0  26706  ang180lem2  26876  angpined  26896  mumullem2  27245  lgsqrmodndvds  27418  gausslemma2dlem0i  27429  2lgs  27472  dchrisum0re  27578  chpdifbnd  27620  pntrlog2bnd  27649  pntibndlem3  27657  pnt3  27677  nofv  27722  nomaxmo  27763  nominmo  27764  noprc  27850  madebday  27994  addsproplem7  28069  negsproplem7  28128  elons2  28352  nbgrval  29538  vtxdginducedm1fi  29746  upgrewlkle2  29808  hiidge0  31302  chsupval  31539  chsupcl  31544  chsupss  31546  ococin  31612  chsupval2  31614  ssjo  31651  h1de2i  31757  pjss2i  31884  pjssmii  31885  sto2i  32441  stge1i  32442  stle0i  32443  stlei  32444  stlesi  32445  stm1i  32447  staddi  32450  stadd3i  32452  golem1  32475  stcltrlem1  32480  mdexchi  32539  chirred  32599  atabsi  32605  abrexdomjm  32707  iocinif  32984  cycpmcl  33297  elrgspnsubrunlem2  33430  voliune  34527  volfiniune  34528  probdif  34718  bnj849  35221  axprALT2  35406  onvf1odlem4  35450  onvf1od  35451  onvfowev  35460  kur14lem9  35565  gonarlem  35745  gonar  35746  goalrlem  35747  goalr  35748  sscoid  36262  limsucncmpi  36806  axtco1from2  36836  axtcond  36839  bj-nnf-spime  37251  bj-axc10  37269  bj-alequex  37270  bj-spimtv  37280  bj-moeub  37335  bj-exlimvmpi  37397  bj-exlimmpi  37398  bj-restpw  37583  bj-isrvec  37787  finxpreclem4  37889  domalom  37899  wl-isseteq  38000  wl-embant  38014  wl-orel12  38015  wl-euequf  38078  poimirlem9  38129  abrexdom  38230  heiborlem10  38320  dvrunz  38454  iss2  38844  equcomi1  39525  ax12eq  39566  ax12el  39567  ax12inda  39573  ax12v2-o  39574  cvrnrefN  39907  pmod1i  40473  pmodN  40475  osumcllem11N  40591  pexmidlem8N  40602  pl42lem3N  40606  cdleme18b  40917  dochexmidlem8  42092  imadomfi  42620  sticksstones3  42766  sn-axprlem3  42838  sn-exelALT  42839  sn-1ne2  42881  remul02  43015  sn-0tie0  43074  pellexlem3  43409  pell1234qrne0  43431  hbtlem6  43707  onsucelab  43841  omabs2  43910  nadd2rabex  43964  or3or  44600  isotone1  44625  isotone2  44626  clsf2  44703  ismnushort  44878  radcnvrat  44891  3impexpbicom  45057  sb5ALT  45102  eexinst01  45103  ax6e2eq  45134  sineq0ALT  45513  tcfr  45540  ssclaxsep  45559  omssaxinf2  45565  nregmodel  45594  fzisoeu  45880  ovnsubaddlem2  47146  ormklocald  47451  natlocalincr  47453  tannpoly  47485  funressnfv  47638  faovcl  47795  sprsymrelfo  48104  clnbgrval  48445  gpgedgiov  48688  gpgedg2ov  48689  gpgedg2iv  48690  pgnioedg1  48731  pgnioedg2  48732  pgnioedg3  48733  pgnioedg4  48734  pgnioedg5  48735  pgnbgreunbgrlem2lem1  48737  pgnbgreunbgrlem2lem2  48738  pgnbgreunbgrlem2lem3  48739  pgnbgreunbgrlem5lem1  48743  pgnbgreunbgrlem5lem2  48744  cznnring  48885  zlmodzxznm  49120  elbigolo1  49180  dignn0flhalflem1  49238  nn0sumshdig  49246  rrx2xpref1o  49341  fonex  49489  vsetrec  50325