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

Theorem simplrl 736
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simplrl  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ps )

Proof of Theorem simplrl
StepHypRef Expression
1 simpl 443 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antlr 707 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  pm2.61da3ne  2559  rmob  3113  disjxiun  4057  f1imass  5830  soisoi  5867  riota5f  6371  tfrlem9a  6444  oeeui  6642  oaabs2  6685  omabs  6687  omxpenlem  7006  fopwdom  7013  frfi  7147  marypha1lem  7231  ordiso2  7275  oismo  7300  wemaplem3  7308  cantnf  7440  isinffi  7670  dfac12lem2  7815  dfac12lem3  7816  infxp  7886  infmap2  7889  infpssrlem5  7978  fin23lem11  7988  fin23lem24  7993  fin23lem26  7996  isf32lem2  8025  isf32lem4  8027  fin1a2lem13  8083  fin1a2s  8085  ttukeylem5  8185  fpwwe2lem12  8308  fpwwe2lem13  8309  wunex2  8405  tskord  8447  prlem934  8702  addid1  9037  cnegex  9038  negeu  9087  add20  9331  divdivdiv  9506  ltmul12a  9657  lediv12a  9694  cru  9783  uzwo3  10358  xleadd1a  10620  xlemul1a  10655  ixxun  10719  ixxss12  10723  mulexpz  11189  leexp1a  11207  expmulnbnd  11280  abs3lem  11869  rexanre  11877  cau3lem  11885  lo1bdd2  12045  o1lo1  12058  rlimclim1  12066  rlimclim  12067  lo1resb  12085  o1resb  12087  rlimcn2  12111  o1of2  12133  o1rlimmul  12139  lo1add  12147  lo1mul  12148  isercolllem1  12185  climcau  12191  summolem2  12236  summo  12237  o1fsum  12318  qredeu  12833  isprm5  12838  pclem  12938  pcqmul  12953  pcexp  12959  pcneg  12973  pcprmpw2  12981  pcadd  12984  prmpwdvds  12998  4sqlem13  13051  vdwlem2  13076  vdwlem7  13081  vdwlem11  13085  vdwlem12  13086  ramval  13102  ramz2  13118  ramcl  13123  imasval  13463  imasdsval  13467  mreexexd  13599  issubc3  13772  idfucl  13804  funcres2c  13824  fucpropd  13900  xpcval  14000  prfval  14022  evlfcl  14045  curf12  14050  curf1cl  14051  curf2  14052  curfcl  14055  curfuncf  14061  curf2ndf  14070  hof2val  14079  hofcl  14082  hofpropd  14090  yonedalem4a  14098  yonedainv  14104  poslubmo  14299  isipodrs  14313  acsmapd  14330  acsinfd  14332  mndpropd  14447  mhmeql  14490  frmdup3  14537  issubg4  14687  ssnmz  14708  sylow2blem3  14982  lsmdisj2  15040  pj1eu  15054  efgredlem  15105  frgpuplem  15130  frgpnabl  15212  dmdprdsplitlem  15321  pgpfac1lem3  15361  pgpfaclem3  15367  rngpropd  15421  dvdsrtr  15483  islmhm2  15844  lmhmpropd  15875  assapropd  16116  coe1tmmul2  16401  prmirredlem  16502  lsmcss  16648  toponmre  16886  restbas  16945  iscncl  17054  cnpdis  17077  lmcnp  17088  dishaus  17166  cmpcovf  17174  hauscmplem  17189  dfcon2  17201  clscon  17212  2ndcctbss  17237  1stccnp  17244  islly2  17266  llyidm  17270  cldllycmp  17277  kgentopon  17289  1stckgenlem  17304  ptpjpre1  17322  ptbasfi  17332  txcls  17355  ptpjopn  17362  xkoccn  17369  txcnp  17370  txcmpb  17394  xkoptsub  17404  xkoco2cn  17408  xkoinjcn  17437  qtopcn  17461  qtoprest  17464  regr1lem  17486  regr1lem2  17487  kqreglem1  17488  qtophmeo  17564  fgabs  17626  hauspwpwf1  17734  flimfnfcls  17775  fclscmp  17777  cnpfcf  17788  ptcmplem4  17801  ptcmplem5  17802  tmdgsum2  17831  tsmsval2  17864  ismet2  17950  blin  18022  metss2lem  18109  methaus  18118  met1stc  18119  met2ndci  18120  metcnp  18139  metcnpi3  18144  nlmvscn  18250  nrginvrcn  18254  nghmcn  18306  xrsxmet  18367  reconnlem1  18383  reconn  18385  xrge0tsms  18391  xmetdcn2  18394  metdscn  18412  addcnlem  18420  mulc1cncf  18461  cncfco  18463  cnheiborlem  18505  cnheibor  18506  nmoleub2lem2  18650  ipcn  18726  iscfil3  18752  cfilfcls  18753  iscmet3  18772  caubl  18786  bcthlem5  18803  minveclem3b  18845  minveclem7  18852  pmltpc  18863  ovolshftlem1  18921  ovolscalem1  18925  ioombl1  18972  uniioombllem6  18996  dyadss  19002  dyaddisjlem  19003  dyadmax  19006  opnmbllem  19009  itg1addlem2  19105  itg2seq  19150  bddmulibl  19246  limcfval  19275  ellimc3  19282  limciun  19297  dveflem  19379  rolle  19390  dvlip2  19395  c1liplem1  19396  dvgt0lem1  19402  dvgt0  19404  dvlt0  19405  dvne0  19411  dvcnvre  19419  dvfsumrlimge0  19430  ftc1lem6  19441  itgsubst  19449  evlslem1  19452  mdegmullem  19517  ply1domn  19562  fta1g  19606  fta1b  19608  dgrlem  19664  coeid  19673  plydivalg  19732  aannenlem1  19761  aalioulem6  19770  ulmcn  19829  abelthlem8  19868  efif1olem4  19960  chordthm  20187  xrlimcnp  20316  isppw2  20406  fsumvma2  20506  perfectlem2  20522  lgsdilem  20614  lgsquad2lem2  20651  lgsquad3  20653  2sqlem5  20660  2sqlem9  20665  rpvmasumlem  20689  dchrisum0flb  20712  pntpbnd  20790  pntibndlem3  20794  pntlem3  20811  pntleml  20813  vacn  21322  ubthlem1  21504  ubthlem3  21506  minvecolem7  21517  chocunii  21935  pjhthmo  21936  pjhthlem2  22026  nmopub2tALT  22544  nmfnleub2  22561  kbass5  22755  mdslmd1lem1  22960  mdslmd1lem2  22961  mdsymlem5  23042  xrofsup  23272  xrge0tsmsd  23360  cnextfval  23412  cnextfun  23414  utoptop  23446  metustto  23495  metustfbas  23499  qqhval2  23561  esumpcvgval  23644  imambfm  23786  ballotlemsf1o  23945  pconcon  24046  conpcon  24050  cvmliftmo  24099  cvmlift2lem10  24127  cvmlift2lem12  24129  cvmlift3lem7  24140  eupath2  24188  dedekind  24368  prodmolem2  24438  axsegcon  24941  axpasch  24955  axeuclidlem  24976  ifscgr  25053  cgrxfr  25064  btwnconn1lem13  25108  ellines  25161  itg2addnclem  25317  itg2addnc  25319  ftc1cnnc  25339  locfincmp  25453  sstotbnd  25647  cntotbnd  25668  ismtyima  25675  heibor1lem  25681  heiborlem10  25692  bfp  25696  rrncmslem  25704  isnacs3  25933  nacsfix  25935  mzpsubst  25974  eldioph2lem2  25988  eldioph2  25989  eldioph2b  25990  diophin  26000  diophun  26001  rencldnfilem  26051  irrapxlem3  26057  irrapxlem5  26059  pell1234qrreccl  26087  pell1234qrmulcl  26088  pell1qrge1  26103  pell1qrgaplem  26106  monotuz  26174  monotoddzzfi  26175  rpexpmord  26181  acongtr  26213  acongrep  26215  jm2.26a  26241  jm2.26lem3  26242  jm2.26  26243  jm2.27b  26247  jm2.27  26249  wepwsolem  26286  fnwe2lem2  26296  dsmmlss  26358  uvcf1  26389  frlmup1  26398  hbtlem5  26480  hbt  26482  mpaaeu  26503  f1otrspeq  26538  psgneu  26577  mamucl  26604  mamulid  26606  mamurid  26607  mamuass  26608  mamudi  26609  mamudir  26610  mamuvs1  26611  mamuvs2  26612  fnchoice  26848  rfcnnnub  26855  stoweidlem14  26911  stoweidlem27  26924  stoweidlem31  26928  stoweidlem34  26931  stoweidlem49  26946  stoweidlem56  26953  4cycl4dv4e  27552  islshpsm  28988  lsatcmp  29011  islshpat  29025  lfl0f  29077  iscvlat2N  29332  ishlat3N  29362  3dim1  29474  islvol5  29586  lvoli2  29588  lncvrelatN  29788  lncmp  29790  paddasslem10  29836  pclfinclN  29957  pexmidlem8N  29984  idltrn  30157  cdleme42keg  30493  cdleme42mgN  30495  cdlemf2  30569  cdlemg2cex  30598  trlcoat  30730  tendoex  30982  erngdvlem4  30998  erngdvlem4-rN  31006  dialss  31054  dibglbN  31174  diblss  31178  dihlsscpre  31242  dihglblem2aN  31301  dihglblem4  31305  dihglblem5  31306  dih1dimatlem  31337  dihglblem6  31348  lcfl7N  31509  lcfrlem9  31558  mapdh9a  31798  hdmapglem7  31940
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
  Copyright terms: Public domain W3C validator