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  6616  fvbr0  6905  fvmptg  6984  funsndifnop  7148  ov3  7576  elovmpo  7659  dford5  7783  limsssuc  7846  tfisi  7855  finds1  7896  frxp  8124  frxp2  8142  frxp3  8149  dfrecs3  8361  tfrlem1  8364  oaordi  8533  oaword2  8540  omeulem1  8569  oeworde  8581  oelim2  8583  nnaordi  8606  oaabs2  8637  limenpsi  9150  dif1en  9156  ordunifi  9260  fidomdm  9301  dffi3  9401  oismo  9512  wdom2d  9552  wdomima2g  9558  epnsym  9588  suc11reg  9598  elom3  9627  cantnfval2  9648  rankunb  9832  rankval4  9849  karden  9898  kardenOLD  9899  cardsn  9974  cardlim  9977  cardprclem  9984  fseqdom  10029  dfac12lem3  10148  kmlem2  10154  kmlem10  10162  cflim2  10265  cfslb2n  10270  fin23lem27  10330  fin23lem17  10340  axcc3  10440  axcc4  10441  acncc  10442  domtriomlem  10444  axdclem2  10522  imadomg  10537  imadomnum  10538  alephval2  10581  alephreg  10591  axextnd  10600  fpwwe2lem9  10648  pwfseq  10673  gch2  10684  axgroth3  10840  inaprc  10845  nlt1pi  10915  indpi  10916  1re  11232  mul02lem2  11411  addrid  11414  fimaxre  12183  fiminre  12186  supaddc  12206  supmul1  12208  rimul  12233  nnge1  12288  zneo  12704  ltweuz  14025  hashrabsn1  14438  hashf1lem2  14521  hash2pwpr  14541  climuni  15639  fsum2d  15857  fsumabs  15888  fsumrlim  15898  fsumo1  15899  fsumiun  15908  fprod2d  16068  efne0d  16183  efne0OLD  16185  ruclem13  16330  dvdslelem  16399  mod2eq1n2dvds  16437  nn0o1gt2  16471  divalglem0  16483  lcmfnnval  16714  prmreclem2  17009  prmreclem3  17010  mreexexd  17736  coaval  18157  xpcco  18271  pltirr  18421  frgpnabllem1  20000  ablfac1eulem  20201  prmgrpsimpgd  20243  mdetunilem9  22842  mretopd  23317  fiuncmp  23629  ptcmpfi  24039  filtop  24081  supnfcls  24246  flimfnfcls  24254  alexsubALTlem2  24274  alexsubALTlem4  24276  trust  24455  rectbntr0  25059  fsumcn  25098  ovoliunlem3  25732  ovolicc2lem4  25748  dyadmax  25826  vitali  25841  itgfsum  26054  dvmptfsum  26202  fta1g  26395  fta1  26538  aannenlem1  26564  aalioulem3  26570  logltb  26837  logdmn0  26877  ang180lem2  27047  angpined  27067  mumullem2  27416  lgsqrmodndvds  27589  gausslemma2dlem0i  27600  2lgs  27643  dchrisum0re  27749  chpdifbnd  27791  pntrlog2bnd  27820  pntibndlem3  27828  pnt3  27848  nofv  27893  nomaxmo  27934  nominmo  27935  noprc  28021  madebday  28165  addsproplem7  28240  negsproplem7  28299  elons2  28523  nbgrval  29796  vtxdginducedm1fi  30004  upgrewlkle2  30066  hiidge0  31579  chsupval  31816  chsupcl  31821  chsupss  31823  ococin  31889  chsupval2  31891  ssjo  31928  h1de2i  32034  pjss2i  32161  pjssmii  32162  sto2i  32718  stge1i  32719  stle0i  32720  stlei  32721  stlesi  32722  stm1i  32724  staddi  32727  stadd3i  32729  golem1  32752  stcltrlem1  32757  mdexchi  32816  chirred  32876  atabsi  32882  abrexdomjm  32982  iocinif  33252  cycpmcl  33556  elrgspnsubrunlem2  33688  voliune  34740  volfiniune  34741  probdif  34931  bnj849  35434  axprALT2  35617  onvf1odlem4  35703  onvf1od  35704  onvfowev  35713  kur14lem9  35793  gonarlem  35973  gonar  35974  goalrlem  35975  goalr  35976  sscoid  36490  limsucncmpi  37064  axtco1from2  37094  axtcond  37097  bj-nnf-spime  37508  bj-axc10  37526  bj-alequex  37527  bj-spimtv  37537  bj-moeub  37592  bj-exlimvmpi  37654  bj-exlimmpi  37655  bj-restpw  37842  bj-isrvec  38046  finxpreclem4  38148  domalom  38158  wl-isseteq  38259  wl-embant  38273  wl-orel12  38274  wl-euequf  38337  poimirlem9  38378  abrexdom  38480  heiborlem10  38570  dvrunz  38704  iss2  39092  equcomi1  39773  ax12eq  39814  ax12el  39815  ax12inda  39821  ax12v2-o  39822  cvrnrefN  40155  pmod1i  40721  pmodN  40723  osumcllem11N  40839  pexmidlem8N  40850  pl42lem3N  40854  cdleme18b  41165  dochexmidlem8  42340  imadomfi  42868  sticksstones3  43014  sn-axprlem3  43088  sn-exelALT  43089  sn-1ne2  43146  remul02  43280  sn-0tie0  43339  pellexlem3  43672  pell1234qrne0  43694  hbtlem6  43970  onsucelab  44104  omabs2  44173  nadd2rabex  44227  or3or  44863  isotone1  44888  isotone2  44889  clsf2  44966  ismnushort  45125  radcnvrat  45138  3impexpbicom  45303  sb5ALT  45348  eexinst01  45349  ax6e2eq  45380  sineq0ALT  45759  tcfr  45786  ssclaxsep  45805  omssaxinf2  45811  nregmodel  45840  fzisoeu  46133  ovnsubaddlem2  47399  ormklocald  47704  funressnfv  47931  faovcl  48088  sprsymrelfo  48397  clnbgrval  48738  gpgedgiov  48981  gpgedg2ov  48982  gpgedg2iv  48983  pgnioedg1  49024  pgnioedg2  49025  pgnioedg3  49026  pgnioedg4  49027  pgnioedg5  49028  pgnbgreunbgrlem2lem1  49030  pgnbgreunbgrlem2lem2  49031  pgnbgreunbgrlem2lem3  49032  pgnbgreunbgrlem5lem1  49036  pgnbgreunbgrlem5lem2  49037  cznnring  49177  zlmodzxznm  49427  elbigolo1  49487  dignn0flhalflem1  49545  nn0sumshdig  49553  rrx2xpref1o  49648  fonex  49795  vsetrec  50629