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

Theorem simp1r 980
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 447 . 2  |-  ( (
ph  /\  ps )  ->  ps )
213ad2ant1 976 1  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpl1r  1007  simpr1r  1013  simp11r  1067  simp21r  1073  simp31r  1079  vtoclgft  2834  funprg  5301  omeulem2  6581  unxpdomlem3  7069  elfiun  7183  cofsmo  7895  isfin2-2  7945  isf32lem9  7987  tskun  8408  tskurn  8411  reclem3pr  8673  dmdcan  9470  lt2msq1  9639  supmullem1  9720  supmul  9722  xaddass2  10570  xlt2add  10580  xmulasslem3  10606  iccsplit  10768  expaddzlem  11145  expaddz  11146  expmulz  11148  limsupgle  11951  o1add  12087  o1mul  12088  o1sub  12089  bitsfzo  12626  sadfval  12643  smufval  12668  prmexpb  12796  4sqlem18  13009  vdwlem10  13037  mrieqv2d  13541  curf1  13999  spwpr4  14340  mndodcong  14857  subgabl  15132  gex2abl  15143  cntzsubr  15577  abvres  15604  lbsind2  15834  lbsextlem2  15912  lbsextg  15915  cnprest  17017  isreg2  17105  fbssfi  17532  hausflimlem  17674  tmdgsum  17778  ssbl  17971  xrsmopn  18318  dvres2  19262  vieta1  19692  aalioulem4  19715  cxpadd  20026  cxpsub  20029  divcxp  20034  cxple2  20044  cxplt2  20045  cxpcn3lem  20087  angcan  20100  ang180lem5  20111  isosctrlem3  20120  chscllem4  22219  measinblem  23547  cvmlift2lem6  23839  dedekind  24082  poseq  24253  brbtwn2  24533  axcontlem4  24595  axcontlem8  24599  linethru  24776  uninqs  25039  truni3  25507  intopcoaconlem3b  25538  prdnei  25573  islimrs  25580  fnctartar  25907  fnctartar2  25908  cnres2  26483  pellfundex  26971  congtr  27052  fzmaxdif  27068  isnumbasgrplem2  27269  matrng  27480  idomsubgmo  27514  stoweidlem31  27780  lcv1  29231  lfl1  29260  lshpkrex  29308  hlrelat3  29601  cvrval3  29602  cvrval4N  29603  athgt  29645  atcvrlln2  29708  atcvrlln  29709  lvolnle3at  29771  lvolnlelpln  29774  4atlem11  29798  4atlem12  29801  2lplnj  29809  dalemddea  29873  cdlema2N  29981  paddasslem2  30010  atmod1i1m  30047  lhp2lt  30190  lhp0lt  30192  lhpexle3lem  30200  lhpj1  30211  lhpmcvr4N  30215  lhpelim  30226  lhpmod2i2  30227  lhpmod6i1  30228  cdlemb2  30230  lhpat  30232  ltrnatb  30326  ltrnel  30328  ltrncnvel  30331  ltrncnv  30335  ltrnmw  30340  trlval2  30352  trljat1  30355  trljat2  30356  trlnidatb  30366  cdlemc1  30380  cdlemc2  30381  cdlemc5  30384  cdlemc6  30385  cdleme0aa  30399  cdleme0b  30401  cdleme0c  30402  cdleme0e  30406  cdleme0fN  30407  cdleme01N  30410  cdleme0ex1N  30412  cdleme0moN  30414  cdleme3g  30423  cdleme3h  30424  cdleme3  30426  cdleme4  30427  cdleme4a  30428  cdleme5  30429  cdleme8  30439  cdleme9  30442  cdleme10  30443  cdleme16aN  30448  cdleme11fN  30453  cdleme11g  30454  cdleme11k  30457  cdleme13  30461  cdleme17c  30477  cdleme17d1  30478  cdleme18c  30482  cdleme22gb  30483  cdlemeda  30487  cdlemednpq  30488  cdlemednuN  30489  cdleme19c  30494  cdleme20aN  30498  cdleme20bN  30499  cdleme20c  30500  cdleme22aa  30528  cdleme22d  30532  cdleme22e  30533  cdleme27cl  30555  cdleme27a  30556  cdleme30a  30567  cdleme42a  30660  cdleme42c  30661  cdlemg2fv2  30789  cdlemg2m  30793  cdlemg4g  30805  cdlemg4  30806  cdlemg6c  30809  cdlemg7aN  30814  cdlemg9a  30821  cdlemg9b  30822  cdlemg10c  30828  cdlemg12a  30832  cdlemg12b  30833  cdlemg17a  30850  cdlemg18b  30868  cdlemg18c  30869  trlcoabs2N  30911  trlcolem  30915  tendoco2  30957  tendoicl  30985  cdlemi1  31007  cdlemi2  31008  cdlemj3  31012  tendocan  31013  cdlemk3  31022  cdlemk4  31023  cdlemk5a  31024  cdlemk9  31028  cdlemk9bN  31029  cdlemk10  31032  cdlemk30  31083  cdlemk31  31085  cdlemk39  31105  cdlemkfid1N  31110  cdlemkfid2N  31112  cdlemk19ylem  31119  cdlemk19xlem  31131  cdlemk53b  31145  cdlemk53  31146  cdlemk55a  31148  cdlemk43N  31152  cdlemk19u1  31158  cdlemm10N  31308  cdlemn2  31385  cdlemn10  31396  dihjustlem  31406  dihord2cN  31411  dihvalcq2  31437  dihopelvalcpre  31438  dihord5b  31449  dihord6b  31450  dihmeetlem2N  31489  dihmeetbclemN  31494  dihmeetlem4preN  31496  dihmeetALTN  31517  dochshpncl  31574  dochsatshpb  31642  hdmapval3N  32031  hgmap11  32095
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator