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

Theorem simplrr 738
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 448 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antlr 708 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  pm2.61da3ne  2678  rmob  3241  disjxiun  4201  isotr  6048  weniso  6067  riota5f  6566  tfrlem9a  6639  oaass  6796  oeeui  6837  oaabs2  6880  resixpfo  7092  omxpenlem  7201  pw2f1olem  7204  fopwdom  7208  fofinf1o  7379  marypha1lem  7430  ordiso2  7476  oismo  7501  ixpiunwdom  7551  cantnf  7641  fseqenlem1  7897  iunfictbso  7987  dfac12lem2  8016  dfac12lem3  8017  infunsdom1  8085  infpssrlem5  8179  fin23lem24  8194  isf32lem2  8226  isf32lem4  8228  isf34lem4  8249  fin1a2lem12  8283  fin1a2lem13  8284  ttukeylem6  8386  fpwwe2lem12  8508  fpwwe2lem13  8509  fpwwe2  8510  winalim2  8563  wunex2  8605  tskord  8647  prlem934  8902  addid1  9238  cnegex  9239  negeu  9288  add20  9532  divdivdiv  9707  ltmul12a  9858  lemul12a  9860  lediv12a  9895  supmul1  9965  cru  9984  uzwo3  10561  xleadd1a  10824  xmullem  10835  xmulgt0  10854  xlemul1a  10859  ixxun  10924  ixxss12  10928  ioodisj  11018  mulexpz  11412  leexp1a  11430  expmulnbnd  11503  hashf1  11698  brfi1uzind  11707  abs3lem  12134  rexanre  12142  cau3lem  12150  limsupgre  12267  limsupbnd2  12269  o1lo1  12323  rlimclim1  12331  rlimclim  12332  rlimcn1  12374  rlimcn2  12376  o1of2  12398  o1rlimmul  12404  lo1add  12412  lo1mul  12413  isercolllem1  12450  climcau  12456  caucvgrlem  12458  caucvgb  12465  summolem2  12502  summo  12503  o1fsum  12584  isprm6  13101  isprm5  13104  rpdvds  13116  pclem  13204  pcqmul  13219  pcexp  13225  pcneg  13239  pcprmpw2  13247  pcadd  13250  pcmpt  13253  4sqlem13  13317  vdwlem2  13342  vdwlem7  13347  vdwlem12  13352  ramval  13368  ramub2  13374  ramz2  13384  ramcl  13389  imasval  13729  imasdsval  13733  mreexexd  13865  acsfn  13876  issubc3  14038  idfucl  14070  funcres2c  14090  isnat  14136  fucpropd  14166  xpcval  14266  xpcco  14272  prfval  14288  evlf2  14307  evlfcl  14311  curf12  14316  curf1cl  14317  curf2  14318  curfcl  14321  curf2ndf  14336  hof2val  14345  hofcl  14348  hofpropd  14356  yonedalem4a  14364  yonedainv  14370  drsdirfi  14387  pospo  14422  poslubmo  14565  isipodrs  14579  acsinfd  14598  mndpropd  14713  mhmeql  14756  gsumvalx  14766  frmdup3  14803  issubg4  14953  ssnmz  14974  conjnmzb  15032  pgpfi  15231  sylow2blem3  15248  slwhash  15250  fislw  15251  sylow3lem2  15254  lsmdisj2  15306  pj1eu  15320  efgredlem  15371  frgpuplem  15396  gexex  15460  frgpnabl  15478  dprdfadd  15570  dpjidcl  15608  pgpfac1lem3  15627  pgpfaclem3  15633  ablfac2  15639  rngpropd  15687  islmhm2  16106  lmhmpropd  16137  lbsextlem4  16225  assapropd  16378  psrval  16421  prmirredlem  16765  lsmcss  16911  pptbas  17064  toponmre  17149  restbas  17214  iscncl  17325  cnrest2  17342  cnpdis  17349  lmcnp  17360  dishaus  17438  cmpcovf  17446  tgcmp  17456  dfcon2  17474  clscon  17485  2ndcctbss  17510  dis2ndc  17515  1stccnp  17517  islly2  17539  cldllycmp  17550  kgentopon  17562  txcls  17628  ptpjopn  17636  dfac14  17642  xkoccn  17643  txcnp  17644  txcmpb  17668  txlm  17672  xkopt  17679  xkoco1cn  17681  xkoco2cn  17682  qtopcn  17738  qtoprest  17741  regr1lem2  17764  xkocnv  17838  qtophmeo  17841  fmfnfmlem4  17981  hausflim  18005  hauspwpwf1  18011  fclscmp  18054  alexsublem  18067  alexsubALTlem2  18071  alexsubALTlem3  18072  ptcmplem3  18077  ptcmplem4  18078  ptcmplem5  18079  cnextfun  18087  tmdgsum2  18118  symgtgp  18123  tsmsval2  18151  tsmsgsum  18160  utoptop  18256  ismet2  18355  blin  18443  metss2lem  18533  methaus  18542  met1stc  18543  met2ndci  18544  prdsxmslem2  18551  metcnp3  18562  metcnpi3  18568  metusttoOLD  18579  metustto  18580  metustfbasOLD  18587  metustfbas  18588  nlmvscn  18715  nrginvrcn  18719  xrsxmet  18832  reconnlem1  18849  reconn  18851  xrge0tsms  18857  xmetdcn2  18860  metdscn  18878  addcnlem  18886  fsumcn  18892  cnheiborlem  18971  cnheibor  18972  bndth  18975  lebnum  18981  nmoleub2lem2  19116  ipcn  19192  iscmet3  19238  caubl  19252  minveclem3b  19321  minveclem7  19328  pjthlem2  19331  pmltpc  19339  volfiniun  19433  ioombl1  19448  dyadss  19478  dyaddisjlem  19479  dyadmax  19482  dyadmbllem  19483  opnmbllem  19485  itg1addlem2  19581  itg10a  19594  mbfi1fseqlem6  19604  itg2seq  19626  itg2monolem1  19634  itg2gt0  19644  itgfsum  19710  limcfval  19751  ellimc2  19756  ellimc3  19758  limcres  19765  limciun  19773  dvres  19790  dveflem  19855  rolle  19866  dvlip2  19871  c1liplem1  19872  dvgt0lem1  19878  dvgt0  19880  dvlt0  19881  dvne0  19887  dvfsumrlimge0  19906  ftc1lem6  19917  itgsubst  19925  evlslem1  19928  mdegmullem  19993  ply1domn  20038  ply1divex  20051  fta1g  20082  fta1b  20084  plyf  20109  dgrlem  20140  coeid  20149  plydivalg  20208  aannenlem1  20237  aalioulem3  20243  aalioulem6  20246  abelthlem8  20347  efif1olem4  20439  chordthm  20670  xrlimcnp  20799  jensen  20819  sqf11  20914  fsumvma2  20990  perfectlem2  21006  lgsdilem  21098  lgsquad2lem2  21135  lgsquad3  21137  2sqlem5  21144  2sqlem9  21149  2sqb  21154  rpvmasumlem  21173  dchrisum0flb  21196  dchrisum0  21206  pntpbnd  21274  pntibndlem3  21278  pntleml  21297  cusgrarn  21460  usgrasscusgra  21484  4cycl4dv4e  21647  eupath2  21694  vacn  22182  blocni  22298  ubthlem3  22366  minvecolem7  22377  chocunii  22795  pjhthmo  22796  pjhthlem2  22886  kbass5  23615  mdsymlem5  23902  xrofsup  24118  gsumpropd2lem  24212  xrge0tsmsd  24215  qqhval2  24358  volmeas  24579  ballotlemfc0  24742  ballotlemfcc  24743  lgamcvglem  24816  lgamcvg2  24831  derangenlem  24849  erdsze2lem1  24881  pconcon  24910  conpcon  24914  cvxscon  24922  cvmliftmolem2  24961  cvmliftmo  24963  cvmlift2lem10  24991  cvmlift2lem12  24993  cvmlift3lem7  25004  dedekind  25179  prodmolem2  25253  poseq  25520  brcgr  25831  brbtwn2  25836  colinearalg  25841  axsegcon  25858  axeuclidlem  25893  axcontlem9  25903  ifscgr  25970  cgrxfr  25981  btwnconn1lem13  26025  btwnconn1lem14  26026  outsideofeq  26056  ellines  26078  supaddc  26228  mblfinlem  26234  mblfinlem2  26235  itg2addnclem  26246  itg2addnc  26249  ftc1cnnc  26269  finminlem  26302  locfincmp  26365  comppfsc  26368  fnejoin2  26379  upixp  26412  filbcmb  26423  sstotbnd2  26464  isbnd3  26474  prdsbnd2  26485  cntotbnd  26486  ismtyima  26493  bfp  26514  rrncmslem  26522  unichnidl  26622  nacsfix  26747  mzpsubst  26786  mzpcompact2lem  26789  eldioph2lem2  26800  eldioph2  26801  eldioph2b  26802  diophin  26812  diophun  26813  irrapxlem3  26868  irrapxlem5  26870  pell1234qrreccl  26898  pell1234qrmulcl  26899  pell14qrdich  26913  pell1qrge1  26914  pell1qrgaplem  26917  monotuz  26985  rpexpmord  26992  acongtr  27024  acongrep  27026  jm2.23  27048  jm2.26a  27052  jm2.26lem3  27053  jm2.26  27054  jm2.27  27060  wepwsolem  27097  fnwe2lem2  27107  kelac1  27119  kercvrlsm  27139  uvcf1  27199  frlmsslsp  27206  frlmup1  27208  hbtlem5  27290  hbt  27292  mpaaeu  27313  f1otrspeq  27348  psgneu  27387  mamucl  27414  mamulid  27416  mamurid  27417  mamuass  27418  mamudi  27419  mamudir  27420  mamuvs1  27421  mamuvs2  27422  cncmpmax  27660  rfcnnnub  27664  stoweidlem31  27737  stoweidlem34  27740  stoweidlem35  27741  stoweidlem49  27755  stoweidlem59  27765  stoweidlem62  27768  fz0fzelfz0  28092  cshweqdif2s  28224  cshwssizelem4a  28236  usg2spthonot1  28300  usgfidegfi  28303  usg2spot2nb  28381  lshpcmp  29713  islshpat  29742  lfl0f  29794  ishlat3N  30079  3dim1  30191  islvol5  30303  lvoli2  30305  lncvrelatN  30505  pclfinclN  30674  pexmidlem8N  30701  idltrn  30874  cdleme42keg  31210  cdleme42mgN  31212  cdlemf2  31286  cdlemg2cex  31315  trlcoat  31447  dihopelvalcpre  31973  dih1dimatlem  32054  dihjatcclem4  32146  lcfl7N  32226  lcfrlem9  32275  mapdh9a  32515  hdmapglem7  32657
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 178  df-an 361
  Copyright terms: Public domain W3C validator