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

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

Proof of Theorem simplrr
StepHypRef Expression
1 simpr 447 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antlr 707 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  pm2.61da3ne  2609  rmob  3165  disjxiun  4122  isotr  5956  weniso  5975  riota5f  6471  tfrlem9a  6544  oaass  6701  oeeui  6742  oaabs2  6785  resixpfo  6997  omxpenlem  7106  pw2f1olem  7109  fopwdom  7113  fofinf1o  7284  marypha1lem  7333  ordiso2  7377  oismo  7402  ixpiunwdom  7452  cantnf  7542  fseqenlem1  7798  iunfictbso  7888  dfac12lem2  7917  dfac12lem3  7918  infunsdom1  7986  infpssrlem5  8080  fin23lem24  8095  isf32lem2  8127  isf32lem4  8129  isf34lem4  8150  fin1a2lem12  8184  fin1a2lem13  8185  ttukeylem6  8288  fpwwe2lem12  8410  fpwwe2lem13  8411  fpwwe2  8412  winalim2  8465  wunex2  8507  tskord  8549  prlem934  8804  addid1  9139  cnegex  9140  negeu  9189  add20  9433  divdivdiv  9608  ltmul12a  9759  lemul12a  9761  lediv12a  9796  supmul1  9866  cru  9885  uzwo3  10462  xleadd1a  10725  xmullem  10736  xmulgt0  10755  xlemul1a  10760  ixxun  10825  ixxss12  10829  ioodisj  10918  mulexpz  11307  leexp1a  11325  expmulnbnd  11398  hashf1  11593  brfi1uzind  11602  abs3lem  12029  rexanre  12037  cau3lem  12045  limsupgre  12162  limsupbnd2  12164  o1lo1  12218  rlimclim1  12226  rlimclim  12227  rlimcn1  12269  rlimcn2  12271  o1of2  12293  o1rlimmul  12299  lo1add  12307  lo1mul  12308  isercolllem1  12345  climcau  12351  caucvgrlem  12353  caucvgb  12360  summolem2  12397  summo  12398  o1fsum  12479  isprm6  12996  isprm5  12999  rpdvds  13011  pclem  13099  pcqmul  13114  pcexp  13120  pcneg  13134  pcprmpw2  13142  pcadd  13145  pcmpt  13148  4sqlem13  13212  vdwlem2  13237  vdwlem7  13242  vdwlem12  13247  ramval  13263  ramub2  13269  ramz2  13279  ramcl  13284  imasval  13624  imasdsval  13628  mreexexd  13760  acsfn  13771  issubc3  13933  idfucl  13965  funcres2c  13985  isnat  14031  fucpropd  14061  xpcval  14161  xpcco  14167  prfval  14183  evlf2  14202  evlfcl  14206  curf12  14211  curf1cl  14212  curf2  14213  curfcl  14216  curf2ndf  14231  hof2val  14240  hofcl  14243  hofpropd  14251  yonedalem4a  14259  yonedainv  14265  drsdirfi  14282  pospo  14317  poslubmo  14460  isipodrs  14474  acsinfd  14493  mndpropd  14608  mhmeql  14651  gsumvalx  14661  frmdup3  14698  issubg4  14848  ssnmz  14869  conjnmzb  14927  pgpfi  15126  sylow2blem3  15143  slwhash  15145  fislw  15146  sylow3lem2  15149  lsmdisj2  15201  pj1eu  15215  efgredlem  15266  frgpuplem  15291  gexex  15355  frgpnabl  15373  dprdfadd  15465  dpjidcl  15503  pgpfac1lem3  15522  pgpfaclem3  15528  ablfac2  15534  rngpropd  15582  islmhm2  16005  lmhmpropd  16036  lbsextlem4  16124  assapropd  16277  psrval  16320  prmirredlem  16663  lsmcss  16809  pptbas  16962  toponmre  17047  restbas  17106  iscncl  17215  cnrest2  17231  cnpdis  17238  lmcnp  17249  dishaus  17327  cmpcovf  17335  tgcmp  17345  dfcon2  17362  clscon  17373  2ndcctbss  17398  dis2ndc  17403  1stccnp  17405  islly2  17427  cldllycmp  17438  kgentopon  17450  txcls  17516  ptpjopn  17523  dfac14  17529  xkoccn  17530  txcnp  17531  txcmpb  17555  txlm  17559  xkopt  17566  xkoco1cn  17568  xkoco2cn  17569  qtopcn  17622  qtoprest  17625  regr1lem2  17648  xkocnv  17722  qtophmeo  17725  fmfnfmlem4  17865  hausflim  17889  hauspwpwf1  17895  fclscmp  17938  alexsublem  17951  alexsubALTlem2  17955  alexsubALTlem3  17956  ptcmplem3  17961  ptcmplem4  17962  ptcmplem5  17963  tmdgsum2  17992  symgtgp  17997  tsmsval2  18025  tsmsgsum  18034  ismet2  18111  blin  18183  metss2lem  18270  methaus  18279  met1stc  18280  met2ndci  18281  prdsxmslem2  18288  metcnp3  18299  metcnpi3  18305  nlmvscn  18411  nrginvrcn  18415  xrsxmet  18528  reconnlem1  18545  reconn  18547  xrge0tsms  18553  xmetdcn2  18556  metdscn  18574  addcnlem  18582  fsumcn  18588  cnheiborlem  18667  cnheibor  18668  bndth  18671  lebnum  18677  nmoleub2lem2  18812  ipcn  18888  iscmet3  18934  caubl  18948  minveclem3b  19007  minveclem7  19014  pjthlem2  19017  pmltpc  19025  volfiniun  19119  ioombl1  19134  dyadss  19164  dyaddisjlem  19165  dyadmax  19168  dyadmbllem  19169  opnmbllem  19171  itg1addlem2  19267  itg10a  19280  mbfi1fseqlem6  19290  itg2seq  19312  itg2monolem1  19320  itg2gt0  19330  itgfsum  19396  limcfval  19437  ellimc2  19442  ellimc3  19444  limcres  19451  limciun  19459  dvres  19476  dveflem  19541  rolle  19552  dvlip2  19557  c1liplem1  19558  dvgt0lem1  19564  dvgt0  19566  dvlt0  19567  dvne0  19573  dvfsumrlimge0  19592  ftc1lem6  19603  itgsubst  19611  evlslem1  19614  mdegmullem  19679  ply1domn  19724  ply1divex  19737  fta1g  19768  fta1b  19770  plyf  19795  dgrlem  19826  coeid  19835  plydivalg  19894  aannenlem1  19923  aalioulem3  19929  aalioulem6  19932  abelthlem8  20033  efif1olem4  20125  chordthm  20356  xrlimcnp  20485  jensen  20505  sqf11  20600  fsumvma2  20676  perfectlem2  20692  lgsdilem  20784  lgsquad2lem2  20821  lgsquad3  20823  2sqlem5  20830  2sqlem9  20835  2sqb  20840  rpvmasumlem  20859  dchrisum0flb  20882  dchrisum0  20892  pntpbnd  20960  pntibndlem3  20964  pntleml  20983  vacn  21580  blocni  21696  ubthlem3  21764  minvecolem7  21775  chocunii  22193  pjhthmo  22194  pjhthlem2  22284  kbass5  23013  mdsymlem5  23300  xrofsup  23526  gsumpropd2lem  23611  xrge0tsmsd  23614  cnextfun  23700  utoptop  23737  metustto  23796  metustfbas  23800  qqhval2  23838  volmeas  24050  ballotlemfc0  24198  ballotlemfcc  24199  lgamcvg2  24287  derangenlem  24305  erdsze2lem1  24337  pconcon  24365  conpcon  24369  cvxscon  24377  cvmliftmolem2  24416  cvmliftmo  24418  cvmlift2lem10  24446  cvmlift2lem12  24448  cvmlift3lem7  24459  eupath2  24491  dedekind  24671  prodmolem2  24745  poseq  24994  brcgr  25270  brbtwn2  25275  colinearalg  25280  axsegcon  25297  axeuclidlem  25332  axcontlem9  25342  ifscgr  25409  cgrxfr  25420  btwnconn1lem13  25464  btwnconn1lem14  25465  outsideofeq  25495  ellines  25517  supaddc  25665  itg2addnclem  25675  itg2addnc  25677  ftc1cnnc  25697  finminlem  25738  locfincmp  25811  comppfsc  25814  fnejoin2  25825  upixp  25910  filbcmb  25939  sstotbnd2  26004  isbnd3  26014  prdsbnd2  26025  cntotbnd  26026  ismtyima  26033  bfp  26054  rrncmslem  26062  unichnidl  26162  nacsfix  26293  mzpsubst  26332  mzpcompact2lem  26335  eldioph2lem2  26346  eldioph2  26347  eldioph2b  26348  diophin  26358  diophun  26359  irrapxlem3  26415  irrapxlem5  26417  pell1234qrreccl  26445  pell1234qrmulcl  26446  pell14qrdich  26460  pell1qrge1  26461  pell1qrgaplem  26464  monotuz  26532  rpexpmord  26539  acongtr  26571  acongrep  26573  jm2.23  26595  jm2.26a  26599  jm2.26lem3  26600  jm2.26  26601  jm2.27  26607  wepwsolem  26644  fnwe2lem2  26654  kelac1  26667  kercvrlsm  26687  uvcf1  26747  frlmsslsp  26754  frlmup1  26756  hbtlem5  26838  hbt  26840  mpaaeu  26861  f1otrspeq  26896  psgneu  26935  mamucl  26962  mamulid  26964  mamurid  26965  mamuass  26966  mamudi  26967  mamudir  26968  mamuvs1  26969  mamuvs2  26970  cncmpmax  27209  rfcnnnub  27213  stoweidlem27  27282  stoweidlem31  27286  stoweidlem34  27289  stoweidlem35  27290  stoweidlem49  27304  stoweidlem59  27314  stoweidlem62  27317  cusgrarn  27624  usgrasscusgra  27648  4cycl4dv4e  27794  lshpcmp  29249  islshpat  29278  lfl0f  29330  ishlat3N  29615  3dim1  29727  islvol5  29839  lvoli2  29841  lncvrelatN  30041  pclfinclN  30210  pexmidlem8N  30237  idltrn  30410  cdleme42keg  30746  cdleme42mgN  30748  cdlemf2  30822  cdlemg2cex  30851  trlcoat  30983  dihopelvalcpre  31509  dih1dimatlem  31590  dihjatcclem4  31682  lcfl7N  31762  lcfrlem9  31811  mapdh9a  32051  hdmapglem7  32193
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