Theorem mpi 21

Description: A nested modus ponens inference. Inference associated with com12 33. (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 16	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mpisyl  22  syl6mpi  68  mp2ani  711  mp3an3  1479  merco2  1769  equs4v  2033  alequexv  2034  equcomiv  2047  equcomi  2050  equvinva  2063  aeveq  2091  spimt  2420  equs4  2450  axc15  2456  2ax6elem  2504  dfeumo  2566  mo4  2596  sbcth  3761  sbcth2  3838  ssun3  4133  ssun4  4134  vn0  4298  elpreqprlem  4833  uniintsn  4952  sepexlem  5264  axprlem2  5397  axprlem4  5399  axpr  5400  axprlem1OLD  5401  axprlem3OLD  5402  axprlem4OLD  5403  axprlem5OLD  5404  axprOLD  5405  axprglem  5409  exel  5417  rext  5431  exss  5446  snopeqop  5491  propssopi  5493  uniopel  5501  opthhausdorff  5502  opthhausdorff0  5503  wefrc  5657  relopabi  5811  relop  5838  dmrnssfld  5966  iss  6039  sofld  6187  ordun  6471  funimass2  6623  fvbr0  6912  fvmptg  6991  funsndifnop  7154  ov3  7582  elovmpo  7665  dford5  7789  limsssuc  7852  tfisi  7861  finds1  7902  frxp  8128  frxp2  8146  frxp3  8153  dfrecs3  8365  tfrlem1  8368  oaordi  8537  oaword2  8544  omeulem1  8573  oeworde  8585  oelim2  8587  nnaordi  8610  oaabs2  8641  limenpsi  9147  dif1en  9153  ordunifi  9257  fidomdm  9298  dffi3  9398  oismo  9509  wdom2d  9549  wdomima2g  9555  epnsym  9585  suc11reg  9595  elom3  9624  cantnfval2  9645  rankunb  9829  rankval4  9846  karden  9895  kardenOLD  9896  cardsn  9971  cardlim  9974  cardprclem  9981  fseqdom  10026  dfac12lem3  10145  kmlem2  10151  kmlem10  10159  cflim2  10262  cfslb2n  10267  fin23lem27  10327  fin23lem17  10337  axcc3  10437  axcc4  10438  acncc  10439  domtriomlem  10441  axdclem2  10519  imadomg  10533  alephval2  10574  alephreg  10584  axextnd  10593  fpwwe2lem9  10641  pwfseq  10666  gch2  10677  axgroth3  10833  inaprc  10838  nlt1pi  10908  indpi  10909  1re  11225  mul02lem2  11404  addrid  11407  fimaxre  12176  fiminre  12179  supaddc  12199  supmul1  12201  rimul  12226  nnge1  12281  zneo  12697  ltweuz  14017  hashrabsn1  14430  hashf1lem2  14513  hash2pwpr  14533  climuni  15629  fsum2d  15847  fsumabs  15878  fsumrlim  15888  fsumo1  15889  fsumiun  15898  fprod2d  16060  efne0d  16175  efne0OLD  16177  ruclem13  16322  dvdslelem  16391  mod2eq1n2dvds  16429  nn0o1gt2  16463  divalglem0  16475  lcmfnnval  16706  prmreclem2  17001  prmreclem3  17002  mreexexd  17728  coaval  18149  xpcco  18263  pltirr  18413  frgpnabllem1  19989  ablfac1eulem  20190  prmgrpsimpgd  20232  mdetunilem9  22829  mretopd  23301  fiuncmp  23613  ptcmpfi  24023  filtop  24065  supnfcls  24230  flimfnfcls  24238  alexsubALTlem2  24258  alexsubALTlem4  24260  trust  24439  rectbntr0  25043  fsumcn  25082  ovoliunlem3  25716  ovolicc2lem4  25732  dyadmax  25810  vitali  25825  itgfsum  26039  dvmptfsum  26187  fta1g  26380  fta1  26522  aannenlem1  26544  aalioulem3  26550  logltb  26818  logdmn0  26858  ang180lem2  27028  angpined  27048  mumullem2  27397  lgsqrmodndvds  27570  gausslemma2dlem0i  27581  2lgs  27624  dchrisum0re  27730  chpdifbnd  27772  pntrlog2bnd  27801  pntibndlem3  27809  pnt3  27829  nofv  27874  nomaxmo  27915  nominmo  27916  noprc  28002  madebday  28146  addsproplem7  28221  negsproplem7  28280  elons2  28504  nbgrval  29746  vtxdginducedm1fi  29954  upgrewlkle2  30016  hiidge0  31523  chsupval  31760  chsupcl  31765  chsupss  31767  ococin  31833  chsupval2  31835  ssjo  31872  h1de2i  31978  pjss2i  32105  pjssmii  32106  sto2i  32662  stge1i  32663  stle0i  32664  stlei  32665  stlesi  32666  stm1i  32668  staddi  32671  stadd3i  32673  golem1  32696  stcltrlem1  32701  mdexchi  32760  chirred  32820  atabsi  32826  abrexdomjm  32926  iocinif  33198  cycpmcl  33502  elrgspnsubrunlem2  33634  voliune  34686  volfiniune  34687  probdif  34877  bnj849  35380  axprALT2  35563  onvf1odlem4  35649  onvf1od  35650  onvfowev  35659  kur14lem9  35745  gonarlem  35925  gonar  35926  goalrlem  35927  goalr  35928  sscoid  36442  limsucncmpi  37015  axtco1from2  37045  axtcond  37048  bj-nnf-spime  37459  bj-axc10  37477  bj-alequex  37478  bj-spimtv  37488  bj-moeub  37543  bj-exlimvmpi  37605  bj-exlimmpi  37606  bj-restpw  37793  bj-isrvec  37997  finxpreclem4  38099  domalom  38109  wl-isseteq  38210  wl-embant  38224  wl-orel12  38225  wl-euequf  38288  poimirlem9  38339  abrexdom  38441  heiborlem10  38531  dvrunz  38665  iss2  39053  equcomi1  39734  ax12eq  39775  ax12el  39776  ax12inda  39782  ax12v2-o  39783  cvrnrefN  40116  pmod1i  40682  pmodN  40684  osumcllem11N  40800  pexmidlem8N  40811  pl42lem3N  40815  cdleme18b  41126  dochexmidlem8  42301  imadomfi  42829  sticksstones3  42975  sn-axprlem3  43049  sn-exelALT  43050  sn-1ne2  43092  remul02  43226  sn-0tie0  43285  pellexlem3  43618  pell1234qrne0  43640  hbtlem6  43916  onsucelab  44050  omabs2  44119  nadd2rabex  44173  or3or  44809  isotone1  44834  isotone2  44835  clsf2  44912  ismnushort  45071  radcnvrat  45084  3impexpbicom  45249  sb5ALT  45294  eexinst01  45295  ax6e2eq  45326  sineq0ALT  45705  tcfr  45732  ssclaxsep  45751  omssaxinf2  45757  nregmodel  45786  fzisoeu  46079  ovnsubaddlem2  47345  ormklocald  47650  natlocalincr  47652  tannpoly  47687  funressnfv  47840  faovcl  47997  sprsymrelfo  48306  clnbgrval  48647  gpgedgiov  48890  gpgedg2ov  48891  gpgedg2iv  48892  pgnioedg1  48933  pgnioedg2  48934  pgnioedg3  48935  pgnioedg4  48936  pgnioedg5  48937  pgnbgreunbgrlem2lem1  48939  pgnbgreunbgrlem2lem2  48940  pgnbgreunbgrlem2lem3  48941  pgnbgreunbgrlem5lem1  48945  pgnbgreunbgrlem5lem2  48946  cznnring  49086  zlmodzxznm  49336  elbigolo1  49396  dignn0flhalflem1  49454  nn0sumshdig  49462  rrx2xpref1o  49557  fonex  49704  vsetrec  50540