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

Theorem simp1r 1021
Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
Assertion
Ref Expression
simp1r  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )

Proof of Theorem simp1r
StepHypRef Expression
1 simpr 461 . 2  |-  ( (
ph  /\  ps )  ->  ps )
213ad2ant1 1017 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
This theorem is referenced by:  simpl1r  1048  simpr1r  1054  simp11r  1108  simp21r  1114  simp31r  1120  vtoclgft  3161  funprg  5636  omeulem2  7232  uniinqs  7391  unxpdomlem3  7726  elfiun  7889  cofsmo  8648  isfin2-2  8698  isf32lem9  8740  tskun  9163  tskurn  9166  reclem3pr  9426  dedekind  9742  dmdcan  10253  lt2msq1  10427  supmullem1  10508  supmul  10510  xaddass2  11441  xlt2add  11451  xmulasslem3  11477  iccsplit  11652  expaddzlem  12176  expaddz  12177  expmulz  12179  limsupgle  13262  o1add  13398  o1mul  13399  o1sub  13400  bitsfzo  13943  sadfval  13960  smufval  13985  prmexpb  14116  4sqlem18  14338  vdwlem10  14366  mrieqv2d  14893  curf1  15351  mndodcong  16369  subgabl  16644  gex2abl  16657  cntzsubr  17256  abvres  17283  lbsind2  17522  lbsextlem2  17600  lbsextg  17603  matrng  18728  mdetunilem8  18904  maducoeval  18924  maducoeval2  18925  madurid  18929  cramerimplem3  18970  pmatcollpw2  19062  cnprest  19572  isreg2  19660  fbssfi  20089  hausflimlem  20231  tmdgsum  20345  ssblps  20676  ssbl  20677  xrsmopn  21068  dvres2  22067  vieta1  22458  aalioulem4  22481  cxpadd  22804  cxpsub  22807  divcxp  22812  cxple2  22822  cxplt2  22823  cxpcn3lem  22865  angcan  22878  ang180lem5  22889  isosctrlem3  22898  brbtwn2  23900  axcontlem4  23962  axcontlem8  23966  clwwlknimp  24468  chscllem4  26250  ogrpinvlt  27392  pstmval  27526  measinblem  27847  cvmlift2lem6  28409  poseq  28926  linethru  29396  cnres2  29878  pellfundex  30442  congtr  30523  fzmaxdif  30539  isnumbasgrplem2  30673  idomsubgmo  30776  upbdrech  31098  mullimc  31174  islptre  31177  mullimcf  31181  neglimc  31205  icccncfext  31242  stoweidlem31  31347  domnmsuppn0  32052  mndpfsupp  32059  lincext3  32147  lcv1  33847  lfl1  33876  lshpkrex  33924  hlrelat3  34217  cvrval3  34218  cvrval4N  34219  athgt  34261  atcvrlln2  34324  atcvrlln  34325  lvolnle3at  34387  lvolnlelpln  34390  4atlem11  34414  4atlem12  34417  2lplnj  34425  dalemddea  34489  cdlema2N  34597  paddasslem2  34626  atmod1i1m  34663  lhp2lt  34806  lhp0lt  34808  lhpexle3lem  34816  lhpj1  34827  lhpmcvr4N  34831  lhpelim  34842  lhpmod2i2  34843  lhpmod6i1  34844  cdlemb2  34846  lhpat  34848  ltrnatb  34942  ltrnel  34944  ltrncnvel  34947  ltrncnv  34951  ltrnmw  34956  trlval2  34968  trljat1  34971  trljat2  34972  trlnidatb  34982  cdlemc1  34996  cdlemc2  34997  cdlemc5  35000  cdlemc6  35001  cdleme0aa  35015  cdleme0b  35017  cdleme0c  35018  cdleme0e  35022  cdleme0fN  35023  cdleme01N  35026  cdleme0ex1N  35028  cdleme0moN  35030  cdleme3g  35039  cdleme3h  35040  cdleme3  35042  cdleme4  35043  cdleme4a  35044  cdleme5  35045  cdleme8  35055  cdleme9  35058  cdleme10  35059  cdleme16aN  35064  cdleme11fN  35069  cdleme11g  35070  cdleme11k  35073  cdleme13  35077  cdleme17c  35093  cdleme17d1  35094  cdleme18c  35098  cdleme22gb  35099  cdlemeda  35103  cdlemednpq  35104  cdlemednuN  35105  cdleme19c  35110  cdleme20aN  35114  cdleme20bN  35115  cdleme20c  35116  cdleme22aa  35144  cdleme22d  35148  cdleme22e  35149  cdleme27cl  35171  cdleme27a  35172  cdleme30a  35183  cdleme42a  35276  cdleme42c  35277  cdlemg2fv2  35405  cdlemg2m  35409  cdlemg4g  35421  cdlemg4  35422  cdlemg6c  35425  cdlemg7aN  35430  cdlemg9a  35437  cdlemg9b  35438  cdlemg10c  35444  cdlemg12a  35448  cdlemg12b  35449  cdlemg17a  35466  cdlemg18b  35484  cdlemg18c  35485  trlcoabs2N  35527  trlcolem  35531  tendoco2  35573  tendoicl  35601  cdlemi1  35623  cdlemi2  35624  cdlemj3  35628  tendocan  35629  cdlemk3  35638  cdlemk4  35639  cdlemk5a  35640  cdlemk9  35644  cdlemk9bN  35645  cdlemk10  35648  cdlemk30  35699  cdlemk31  35701  cdlemk39  35721  cdlemkfid1N  35726  cdlemkfid2N  35728  cdlemk19ylem  35735  cdlemk19xlem  35747  cdlemk53b  35761  cdlemk53  35762  cdlemk55a  35764  cdlemk43N  35768  cdlemk19u1  35774  cdlemm10N  35924  cdlemn2  36001  cdlemn10  36012  dihjustlem  36022  dihord2cN  36027  dihvalcq2  36053  dihopelvalcpre  36054  dihord5b  36065  dihord6b  36066  dihmeetlem2N  36105  dihmeetbclemN  36110  dihmeetlem4preN  36112  dihmeetALTN  36133  dochshpncl  36190  dochsatshpb  36258  hdmapval3N  36647  hgmap11  36711
  Copyright terms: Public domain W3C validator