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  697  mp3an3  1447  merco2  1731  equs4v  1996  alequexv  1997  equcomiv  2010  equcomi  2013  equvinva  2026  aeveq  2052  spimt  2380  equs4  2410  axc15  2416  2ax6elem  2464  dfeumo  2526  mo4  2555  pm13.183  3652  sbcth  3789  sbcth2  3874  ssun3  4170  ssun4  4171  elpreqprlem  4862  uniintsn  4985  axprlem1  5417  axprlem2  5418  axprlem3  5419  axprlem4  5420  axprlem5  5421  axpr  5422  exel  5429  rext  5444  exss  5459  snopeqop  5502  propssopi  5504  uniopel  5512  opthhausdorff  5513  opthhausdorff0  5514  wefrc  5666  relopabi  5818  relop  5847  dmrnssfld  5967  iss  6033  sofld  6185  ordun  6467  funimass2  6630  fvbr0  6920  fvmptg  6997  funsndifnop  7154  ov3  7578  elovmpo  7660  dford5  7780  limsssuc  7848  tfisi  7857  finds1  7901  frxp  8125  frxp2  8143  frxp3  8150  wfrlem5OLD  8327  wfrlem16OLD  8338  dfrecs3  8386  dfrecs3OLD  8387  tfrlem1  8390  oaordi  8560  oaword2  8567  omeulem1  8596  oeworde  8607  oelim2  8609  nnaordi  8632  oaabs2  8663  0domgOLD  9117  limenpsi  9168  dif1en  9176  dif1enOLD  9178  enp1iOLD  9296  findcard2OLD  9300  ordunifi  9309  fidomdm  9345  dffi3  9446  oismo  9555  wdom2d  9595  wdomima2g  9601  epnsym  9624  suc11reg  9634  elom3  9663  cantnfval2  9684  rankunb  9865  rankval4  9882  karden  9910  cardsn  9984  cardlim  9987  cardprclem  9994  fseqdom  10041  dfac12lem3  10160  kmlem2  10166  kmlem10  10174  cflim2  10278  cfslb2n  10283  fin23lem27  10343  fin23lem17  10353  axcc3  10453  axcc4  10454  acncc  10455  domtriomlem  10457  axdclem2  10535  imadomg  10549  alephval2  10587  alephreg  10597  axextnd  10606  fpwwe2lem9  10654  pwfseq  10679  gch2  10690  axgroth3  10846  inaprc  10851  nlt1pi  10921  indpi  10922  1re  11236  mul02lem2  11413  addrid  11416  fimaxre  12180  fiminre  12183  supaddc  12203  supmul1  12205  inelr  12224  rimul  12225  nnge1  12262  zneo  12667  ltweuz  13950  hashrabsn1  14357  hashf1lem2  14441  hash2pwpr  14461  climuni  15520  fsum2d  15741  fsumabs  15771  fsumrlim  15781  fsumo1  15782  fsumiun  15791  fprod2d  15949  efne0  16065  ruclem13  16210  dvdslelem  16277  mod2eq1n2dvds  16315  nn0o1gt2  16349  divalglem0  16361  lcmfnnval  16586  prmreclem2  16877  prmreclem3  16878  mreexexd  17619  coaval  18048  xpcco  18165  pltirr  18318  frgpnabllem1  19819  ablfac1eulem  20020  prmgrpsimpgd  20062  mdetunilem9  22509  mretopd  22983  fiuncmp  23295  ptcmpfi  23704  filtop  23746  supnfcls  23911  flimfnfcls  23919  alexsubALTlem2  23939  alexsubALTlem4  23941  trust  24121  rectbntr0  24735  fsumcn  24775  ovoliunlem3  25420  ovolicc2lem4  25436  dyadmax  25514  vitali  25529  itgfsum  25743  dvmptfsum  25894  fta1g  26091  fta1  26230  aannenlem1  26250  aalioulem3  26256  logltb  26521  logdmn0  26561  ang180lem2  26729  angpined  26749  mumullem2  27099  lgsqrmodndvds  27273  gausslemma2dlem0i  27284  2lgs  27327  dchrisum0re  27433  chpdifbnd  27475  pntrlog2bnd  27504  pntibndlem3  27512  pnt3  27532  nofv  27577  nomaxmo  27618  nominmo  27619  noprc  27699  madebday  27813  addsproplem7  27879  negsproplem7  27933  elons2  28138  nbgrval  29136  vtxdginducedm1fi  29345  upgrewlkle2  29407  hiidge0  30895  chsupval  31132  chsupcl  31137  chsupss  31139  ococin  31205  chsupval2  31207  ssjo  31244  h1de2i  31350  pjss2i  31477  pjssmii  31478  sto2i  32034  stge1i  32035  stle0i  32036  stlei  32037  stlesi  32038  stm1i  32040  staddi  32043  stadd3i  32045  golem1  32068  stcltrlem1  32073  mdexchi  32132  chirred  32192  atabsi  32198  abrexdomjm  32288  iocinif  32533  cycpmcl  32815  voliune  33784  volfiniune  33785  probdif  33976  bnj849  34492  kur14lem9  34760  gonarlem  34940  gonar  34941  goalrlem  34942  goalr  34943  sscoid  35445  limsucncmpi  35865  bj-axc10  36196  bj-alequex  36197  bj-spimtv  36207  bj-moeub  36262  bj-exlimvmpi  36325  bj-exlimmpi  36326  bj-restpw  36507  bj-isrvec  36709  finxpreclem4  36809  domalom  36819  wl-embant  36913  wl-orel12  36914  wl-euequf  36976  poimirlem9  37037  abrexdom  37138  heiborlem10  37228  dvrunz  37362  iss2  37752  equcomi1  38309  ax12eq  38350  ax12el  38351  ax12inda  38357  ax12v2-o  38358  cvrnrefN  38691  pmod1i  39258  pmodN  39260  osumcllem11N  39376  pexmidlem8N  39387  pl42lem3N  39391  cdleme18b  39702  dochexmidlem8  40877  imadomfi  41410  sticksstones3  41552  sn-axprlem3  41625  sn-exelALT  41626  sn-1ne2  41762  efne0d  41830  remul02  41882  sn-0tie0  41916  pellexlem3  42173  pell1234qrne0  42195  hbtlem6  42475  onsucelab  42615  omabs2  42684  nadd2rabex  42738  or3or  43376  isotone1  43401  isotone2  43402  clsf2  43479  ismnushort  43661  radcnvrat  43674  3impexpbicom  43841  sb5ALT  43887  eexinst01  43888  ax6e2eq  43919  sineq0ALT  44299  fzisoeu  44605  ovnsubaddlem2  45882  natlocalincr  46185  tworepnotupword  46195  funressnfv  46348  faovcl  46503  sprsymrelfo  46760  cznnring  47247  zlmodzxznm  47488  elbigolo1  47553  dignn0flhalflem1  47611  nn0sumshdig  47619  rrx2xpref1o  47714  vsetrec  48057