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

Theorem simp1r 1039
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 467 . 2  |-  ( (
ph  /\  ps )  ->  ps )
213ad2ant1 1035 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  simpl1r  1066  simpr1r  1072  simp11r  1126  simp21r  1132  simp31r  1138  vtoclgft  3108  funprg  5650  omeulem2  7310  uniinqs  7469  unxpdomlem3  7804  elfiun  7970  cofsmo  8725  isfin2-2  8775  isf32lem9  8817  tskun  9237  tskurn  9240  reclem3pr  9500  dedekind  9823  dmdcan  10345  lt2msq1  10518  supmullem1  10605  supmul  10607  xaddass2  11565  xlt2add  11575  xmulasslem3  11601  iccsplit  11794  expaddzlem  12347  expaddz  12348  expmulz  12350  limsupgle  13584  o1add  13726  o1mul  13727  o1sub  13728  bitsfzo  14458  sadfval  14475  smufval  14500  prmexpb  14719  4sqlem18OLD  14955  4sqlem18  14961  vdwlem10  14989  mrieqv2d  15594  curf1  16159  mndodcong  17240  subgabl  17525  gex2abl  17538  cntzsubr  18089  abvres  18116  lbsind2  18353  lbsextlem2  18431  lbsextg  18434  matring  19517  mdetunilem8  19693  maducoeval  19713  maducoeval2  19714  madurid  19718  cramerimplem3  19759  pmatcollpw2  19851  pm2mpf1  19872  cnprest  20354  isreg2  20442  fbssfi  20901  hausflimlem  21043  tmdgsum  21159  ssblps  21486  ssbl  21487  xrsmopn  21879  dvres2  22916  vieta1  23314  aalioulem4  23340  efgh  23539  cxpadd  23673  cxpsub  23676  divcxp  23681  cxple2  23691  cxplt2  23692  cxpcn3lem  23736  angcan  23780  ang180lem5  23791  isosctrlem3  23798  brbtwn2  24984  axcontlem4  25046  axcontlem8  25050  clwwlknimp  25553  chscllem4  27342  ogrpinvlt  28536  pstmval  28747  measinblem  29091  cvmlift2lem6  30080  poseq  30540  linethru  30969  cnres2  32140  lcv1  32652  lfl1  32681  lshpkrex  32729  hlrelat3  33022  cvrval3  33023  cvrval4N  33024  athgt  33066  atcvrlln2  33129  atcvrlln  33130  lvolnle3at  33192  lvolnlelpln  33195  4atlem11  33219  4atlem12  33222  2lplnj  33230  dalemddea  33294  cdlema2N  33402  paddasslem2  33431  atmod1i1m  33468  lhp2lt  33611  lhp0lt  33613  lhpexle3lem  33621  lhpj1  33632  lhpmcvr4N  33636  lhpelim  33647  lhpmod2i2  33648  lhpmod6i1  33649  cdlemb2  33651  lhpat  33653  ltrnatb  33747  ltrnel  33749  ltrncnvel  33752  ltrncnv  33756  ltrnmwOLD  33762  trlval2  33774  trljat1  33777  trljat2  33778  trlnidatb  33788  cdlemc1  33802  cdlemc2  33803  cdlemc5  33806  cdlemc6  33807  cdleme0aa  33821  cdleme0b  33823  cdleme0c  33824  cdleme0e  33828  cdleme0fN  33829  cdleme01N  33832  cdleme0ex1N  33834  cdleme0moN  33836  cdleme3g  33845  cdleme3h  33846  cdleme3  33848  cdleme4  33849  cdleme4a  33850  cdleme5  33851  cdleme8  33861  cdleme9  33864  cdleme10  33865  cdleme16aN  33870  cdleme11fN  33875  cdleme11g  33876  cdleme11k  33879  cdleme13  33883  cdleme17c  33899  cdleme17d1  33900  cdleme18c  33904  cdleme22gb  33905  cdlemeda  33909  cdlemednpq  33910  cdlemednuN  33911  cdleme19c  33917  cdleme20aN  33921  cdleme20bN  33922  cdleme20c  33923  cdleme22aa  33951  cdleme22d  33955  cdleme22e  33956  cdleme27cl  33978  cdleme27a  33979  cdleme30a  33990  cdleme42a  34083  cdleme42c  34084  cdlemg2fv2  34212  cdlemg2m  34216  cdlemg4g  34228  cdlemg4  34229  cdlemg6c  34232  cdlemg7aN  34237  cdlemg9a  34244  cdlemg9b  34245  cdlemg10c  34251  cdlemg12a  34255  cdlemg12b  34256  cdlemg17a  34273  cdlemg18b  34291  cdlemg18c  34292  trlcoabs2N  34334  trlcolem  34338  tendoco2  34380  tendoicl  34408  cdlemi1  34430  cdlemi2  34431  cdlemj3  34435  tendocan  34436  cdlemk3  34445  cdlemk4  34446  cdlemk5a  34447  cdlemk9  34451  cdlemk9bN  34452  cdlemk10  34455  cdlemk30  34506  cdlemk31  34508  cdlemk39  34528  cdlemkfid1N  34533  cdlemkfid2N  34535  cdlemk19ylem  34542  cdlemk19xlem  34554  cdlemk53b  34568  cdlemk53  34569  cdlemk55a  34571  cdlemk43N  34575  cdlemk19u1  34581  cdlemm10N  34731  cdlemn2  34808  cdlemn10  34819  dihjustlem  34829  dihord2cN  34834  dihvalcq2  34860  dihopelvalcpre  34861  dihord5b  34872  dihord6b  34873  dihmeetlem2N  34912  dihmeetbclemN  34917  dihmeetlem4preN  34919  dihmeetALTN  34940  dochshpncl  34997  dochsatshpb  35065  hdmapval3N  35454  hgmap11  35518  pellfundex  35779  congtr  35860  fzmaxdif  35876  isnumbasgrplem2  36008  idomsubgmo  36117  upbdrech  37561  suplesup  37600  mullimc  37734  islptre  37737  mullimcf  37741  neglimc  37766  icccncfext  37803  dvmptfprod  37858  stoweidlem31  37930  opnvonmbllem2  38493  uhgr2edg  39339  domnmsuppn0  40427  mndpfsupp  40434  lincext3  40522
  Copyright terms: Public domain W3C validator