MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpi Unicode version

Theorem mpi 17
Description: A nested modus ponens inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)
Hypotheses
Ref Expression
mpi.1  |-  ps
mpi.2  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
mpi  |-  ( ph  ->  ch )

Proof of Theorem mpi
StepHypRef Expression
1 mpi.1 . . 3  |-  ps
21a1i 11 . 2  |-  ( ph  ->  ps )
3 mpi.2 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
42, 3mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  mp2ALT  18  syl6mpi  60  mp2ani  660  mp3an3  1268  3impexpbicom  1373  ee10  1382  merco2  1507  equcomi  1687  19.8a  1758  equs4  1951  spimt  1953  ax10OLD  1998  equveliOLD  2043  ax11v2  2045  ax11eq  2243  ax11el  2244  ax11inda  2250  ax11v2-o  2251  pm13.183  3036  sbcth  3135  sbcth2  3204  ssun3  3472  ssun4  3473  uneqdifeq  3676  ralf0  3694  uniintsn  4047  rext  4372  exss  4386  uniopel  4420  wefrc  4536  ordun  4642  limsssuc  4789  tfisi  4797  finds1  4833  relop  4982  dmrnssfld  5088  iss  5148  sofld  5277  relcoi1  5357  nfunv  5443  funimass2  5486  fvbr0  5711  fvmptg  5763  fovcl  6134  ov3  6169  elovmpt2  6250  frxp  6415  oaordi  6748  oaword2  6755  omeulem1  6784  oeworde  6795  oelim2  6797  nnaordi  6820  oaabs2  6847  0domg  7193  limenpsi  7241  enp1i  7302  findcard2  7307  ordunifi  7316  fidomdm  7347  dffi3  7394  oismo  7465  wdom2d  7504  wdomima2g  7510  suc11reg  7530  elom3  7559  cantnfval2  7580  rankunb  7732  rankval4  7749  karden  7775  cardsn  7812  cardlim  7815  cardprclem  7822  fseqdom  7863  dfac12lem3  7981  kmlem2  7987  kmlem10  7995  cflim2  8099  cfslb2n  8104  fin23lem27  8164  axcc3  8274  axcc4  8275  acncc  8276  domtriomlem  8278  axdclem2  8356  imadomg  8368  alephval2  8403  alephreg  8413  axextnd  8422  fpwwe2lem10  8470  pwfseq  8495  gch2  8510  axgroth3  8662  inaprc  8667  nlt1pi  8739  indpi  8740  1re  9046  mul02lem2  9199  addid1  9202  fimaxre  9911  supmul1  9929  inelr  9946  rimul  9947  nnge1  9982  zneo  10308  uzindOLD  10320  ltweuz  11256  hashf1lem2  11660  climuni  12301  fsum2d  12510  fsumabs  12535  fsumrlim  12545  fsumo1  12546  fsumiun  12555  efne0  12653  ruclem13  12796  dvdslelem  12849  divalglem0  12868  prmreclem2  13240  prmreclem3  13241  mreexexd  13828  coaval  14178  xpcco  14235  pltirr  14375  frgpnabllem1  15439  ablfac1eulem  15585  mretopd  17111  fiuncmp  17421  ptcmpfi  17798  filtop  17840  supnfcls  18005  flimfnfcls  18013  alexsubALTlem2  18032  alexsubALTlem4  18034  trust  18212  rectbntr0  18816  fsumcn  18853  ovoliunlem3  19353  ovolicc2lem4  19369  dyadmax  19443  vitali  19458  itgfsum  19671  dvmptfsum  19812  fta1g  20043  fta1  20178  aannenlem1  20198  aalioulem3  20204  logltb  20447  logdmn0  20484  ang180lem2  20605  angpined  20624  mumullem2  20916  dchrisum0re  21160  chpdifbnd  21202  pntrlog2bnd  21231  pntibndlem3  21239  pnt3  21259  nbgraop  21389  isuvtx  21450  dvrunz  21974  hiidge0  22553  chsupval  22790  chsupcl  22795  chsupss  22797  ococin  22863  chsupval2  22865  ssjo  22902  h1de2i  23008  pjss2i  23135  pjssmii  23136  sto2i  23693  stge1i  23694  stle0i  23695  stlei  23696  stlesi  23697  stm1i  23699  staddi  23702  stadd3i  23704  golem1  23727  stcltrlem1  23732  mdexchi  23791  chirred  23851  atabsi  23857  abrexdomjm  23941  ifbieq12d2  23955  iocinif  24097  voliune  24538  volfiniune  24539  sibfof  24607  probdif  24631  kur14lem9  24853  relexp1  25084  fprod2d  25258  wfrlem5  25474  wfrlem16  25485  tfrALTlem  25490  frrlem5  25499  nofv  25525  noprc  25549  dffun10  25667  limsucncmpi  26099  wl-adnestantALT  26122  supaddc  26137  abrexdom  26322  heiborlem10  26419  pellexlem3  26784  pell1234qrne0  26806  hbtlem6  27201  funressnfv  27859  faovcl  27931  frgrancvvdeqlem4  28136  sb5ALT  28320  eexinst01  28321  a9e2eq  28355  bnj849  29002  ax10NEW7  29179  equveliNEW7  29232  ax11v2NEW7  29234  cvrnrefN  29765  pmod1i  30330  pmodN  30332  osumcllem11N  30448  pexmidlem8N  30459  pl42lem3N  30463  cdleme18b  30774  dochexmidlem8  31950
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator