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  2415  equs4  2445  axc15  2451  2ax6elem  2499  dfeumo  2561  mo4  2591  sbcth  3754  sbcth2  3831  ssun3  4126  ssun4  4127  vn0  4291  elpreqprlem  4826  uniintsn  4945  sepexlem  5256  axprlem2  5389  axprlem4  5391  axpr  5392  axprlem1OLD  5393  axprlem3OLD  5394  axprlem4OLD  5395  axprlem5OLD  5396  axprOLD  5397  axprglem  5401  exel  5409  rext  5423  exss  5438  snopeqop  5483  propssopi  5485  uniopel  5493  opthhausdorff  5494  opthhausdorff0  5495  wefrc  5649  relopabi  5803  relop  5830  dmrnssfld  5958  iss  6031  sofld  6180  ordun  6464  funimass2  6617  fvbr0  6906  fvmptg  6985  funsndifnop  7149  ov3  7577  elovmpo  7660  dford5  7784  limsssuc  7847  tfisi  7856  finds1  7897  frxp  8125  frxp2  8143  frxp3  8150  dfrecs3  8362  tfrlem1  8365  oaordi  8536  oaword2  8543  omeulem1  8572  oeworde  8584  oelim2  8586  nnaordi  8609  oaabs2  8640  limenpsi  9153  dif1en  9159  ordunifi  9263  fidomdm  9304  dffi3  9404  oismo  9515  wdom2d  9555  wdomima2g  9561  epnsym  9591  suc11reg  9601  elom3  9630  cantnfval2  9651  rankunb  9835  rankval4  9852  karden  9901  kardenOLD  9902  cardsn  9977  cardlim  9980  cardprclem  9987  fseqdom  10032  dfac12lem3  10151  kmlem2  10157  kmlem10  10165  cflim2  10268  cfslb2n  10273  fin23lem27  10333  fin23lem17  10343  axcc3  10443  axcc4  10444  acncc  10445  domtriomlem  10447  axdclem2  10525  imadomg  10540  imadomnum  10541  alephval2  10584  alephreg  10594  axextnd  10603  fpwwe2lem9  10651  pwfseq  10676  gch2  10687  axgroth3  10843  inaprc  10848  nlt1pi  10918  indpi  10919  1re  11235  mul02lem2  11414  addrid  11417  fimaxre  12186  fiminre  12189  supaddc  12209  supmul1  12211  rimul  12236  nnge1  12291  zneo  12707  ltweuz  14028  hashrabsn1  14441  hashf1lem2  14524  hash2pwpr  14544  climuni  15642  fsum2d  15860  fsumabs  15891  fsumrlim  15901  fsumo1  15902  fsumiun  15911  fprod2d  16071  efne0d  16186  efne0OLD  16188  ruclem13  16333  dvdslelem  16402  mod2eq1n2dvds  16440  nn0o1gt2  16474  divalglem0  16486  lcmfnnval  16717  prmreclem2  17012  prmreclem3  17013  mreexexd  17739  coaval  18160  xpcco  18274  pltirr  18424  frgpnabllem1  20003  ablfac1eulem  20204  prmgrpsimpgd  20246  mdetunilem9  22845  mretopd  23320  fiuncmp  23632  ptcmpfi  24042  filtop  24084  supnfcls  24249  flimfnfcls  24257  alexsubALTlem2  24277  alexsubALTlem4  24279  trust  24458  rectbntr0  25062  fsumcn  25101  ovoliunlem3  25735  ovolicc2lem4  25751  dyadmax  25829  vitali  25844  itgfsum  26057  dvmptfsum  26205  fta1g  26398  fta1  26541  aannenlem1  26567  aalioulem3  26573  logltb  26840  logdmn0  26880  ang180lem2  27050  angpined  27070  mumullem2  27419  lgsqrmodndvds  27592  gausslemma2dlem0i  27603  2lgs  27646  dchrisum0re  27752  chpdifbnd  27794  pntrlog2bnd  27823  pntibndlem3  27831  pnt3  27851  nofv  27896  nomaxmo  27937  nominmo  27938  noprc  28024  madebday  28168  addsproplem7  28243  negsproplem7  28302  elons2  28526  nbgrval  29799  vtxdginducedm1fi  30007  upgrewlkle2  30069  hiidge0  31582  chsupval  31819  chsupcl  31824  chsupss  31826  ococin  31892  chsupval2  31894  ssjo  31931  h1de2i  32037  pjss2i  32164  pjssmii  32165  sto2i  32721  stge1i  32722  stle0i  32723  stlei  32724  stlesi  32725  stm1i  32727  staddi  32730  stadd3i  32732  golem1  32755  stcltrlem1  32760  mdexchi  32819  chirred  32879  atabsi  32885  abrexdomjm  32985  iocinif  33255  cycpmcl  33559  elrgspnsubrunlem2  33691  voliune  34743  volfiniune  34744  probdif  34934  bnj849  35437  axprALT2  35620  onvf1odlem4  35706  onvf1od  35707  onvfowev  35716  kur14lem9  35796  gonarlem  35976  gonar  35977  goalrlem  35978  goalr  35979  sscoid  36493  limsucncmpi  37067  axtco1from2  37097  axtcond  37100  bj-nnf-spime  37511  bj-axc10  37529  bj-alequex  37530  bj-spimtv  37540  bj-moeub  37595  bj-exlimvmpi  37657  bj-exlimmpi  37658  bj-restpw  37845  bj-isrvec  38049  finxpreclem4  38151  domalom  38161  wl-isseteq  38262  wl-embant  38276  wl-orel12  38277  wl-euequf  38340  poimirlem9  38381  abrexdom  38483  heiborlem10  38573  dvrunz  38707  iss2  39095  equcomi1  39776  ax12eq  39817  ax12el  39818  ax12inda  39824  ax12v2-o  39825  cvrnrefN  40158  pmod1i  40724  pmodN  40726  osumcllem11N  40842  pexmidlem8N  40853  pl42lem3N  40857  cdleme18b  41168  dochexmidlem8  42343  imadomfi  42871  sticksstones3  43017  sn-axprlem3  43091  sn-exelALT  43092  sn-1ne2  43149  remul02  43283  sn-0tie0  43342  pellexlem3  43675  pell1234qrne0  43697  hbtlem6  43973  onsucelab  44107  omabs2  44176  nadd2rabex  44230  or3or  44866  isotone1  44891  isotone2  44892  clsf2  44969  ismnushort  45128  radcnvrat  45141  3impexpbicom  45306  sb5ALT  45351  eexinst01  45352  ax6e2eq  45383  sineq0ALT  45762  tcfr  45789  ssclaxsep  45808  omssaxinf2  45814  nregmodel  45843  fzisoeu  46136  ovnsubaddlem2  47402  ormklocald  47707  funressnfv  47934  faovcl  48091  sprsymrelfo  48400  clnbgrval  48741  gpgedgiov  48984  gpgedg2ov  48985  gpgedg2iv  48986  pgnioedg1  49027  pgnioedg2  49028  pgnioedg3  49029  pgnioedg4  49030  pgnioedg5  49031  pgnbgreunbgrlem2lem1  49033  pgnbgreunbgrlem2lem2  49034  pgnbgreunbgrlem2lem3  49035  pgnbgreunbgrlem5lem1  49039  pgnbgreunbgrlem5lem2  49040  cznnring  49180  zlmodzxznm  49430  elbigolo1  49490  dignn0flhalflem1  49548  nn0sumshdig  49556  rrx2xpref1o  49651  fonex  49798  vsetrec  50632