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  2526  rmob  3079  disjxiun  4020  isotr  5833  weniso  5852  riota5f  6329  tfrlem9a  6402  oaass  6559  oeeui  6600  oaabs2  6643  resixpfo  6854  omxpenlem  6963  pw2f1olem  6966  fopwdom  6970  fofinf1o  7137  marypha1lem  7186  ordiso2  7230  oismo  7255  ixpiunwdom  7305  cantnf  7395  fseqenlem1  7651  iunfictbso  7741  dfac12lem2  7770  dfac12lem3  7771  infunsdom1  7839  infpssrlem5  7933  fin23lem24  7948  isf32lem2  7980  isf32lem4  7982  isf34lem4  8003  fin1a2lem12  8037  fin1a2lem13  8038  ttukeylem6  8141  fpwwe2lem12  8263  fpwwe2lem13  8264  fpwwe2  8265  winalim2  8318  wunex2  8360  tskord  8402  prlem934  8657  addid1  8992  cnegex  8993  negeu  9042  add20  9286  divdivdiv  9461  ltmul12a  9612  lemul12a  9614  lediv12a  9649  supmul1  9719  cru  9738  uzwo3  10311  xleadd1a  10573  xmullem  10584  xmulgt0  10603  xlemul1a  10608  ixxun  10672  ixxss12  10676  ioodisj  10765  mulexpz  11142  leexp1a  11160  expmulnbnd  11233  hashf1  11395  abs3lem  11822  rexanre  11830  cau3lem  11838  limsupgre  11955  limsupbnd2  11957  o1lo1  12011  rlimclim1  12019  rlimclim  12020  rlimcn1  12062  rlimcn2  12064  o1of2  12086  o1rlimmul  12092  lo1add  12100  lo1mul  12101  isercolllem1  12138  climcau  12144  caucvgrlem  12145  caucvgb  12152  summolem2  12189  summo  12190  o1fsum  12271  isprm6  12788  isprm5  12791  rpdvds  12803  pclem  12891  pcqmul  12906  pcexp  12912  pcneg  12926  pcprmpw2  12934  pcadd  12937  pcmpt  12940  4sqlem13  13004  vdwlem2  13029  vdwlem7  13034  vdwlem12  13039  ramval  13055  ramub2  13061  ramz2  13071  ramcl  13076  imasval  13414  imasdsval  13418  mreexexd  13550  acsfn  13561  issubc3  13723  idfucl  13755  funcres2c  13775  isnat  13821  fucpropd  13851  xpcval  13951  xpcco  13957  prfval  13973  evlf2  13992  evlfcl  13996  curf12  14001  curf1cl  14002  curf2  14003  curfcl  14006  curf2ndf  14021  hof2val  14030  hofcl  14033  hofpropd  14041  yonedalem4a  14049  yonedainv  14055  drsdirfi  14072  pospo  14107  poslubmo  14250  isipodrs  14264  acsinfd  14283  mndpropd  14398  mhmeql  14441  gsumvalx  14451  frmdup3  14488  issubg4  14638  ssnmz  14659  conjnmzb  14717  pgpfi  14916  sylow2blem3  14933  slwhash  14935  fislw  14936  sylow3lem2  14939  lsmdisj2  14991  pj1eu  15005  efgredlem  15056  frgpuplem  15081  gexex  15145  frgpnabl  15163  dprdfadd  15255  dpjidcl  15293  pgpfac1lem3  15312  pgpfaclem3  15318  ablfac2  15324  rngpropd  15372  islmhm2  15795  lmhmpropd  15826  lbsextlem4  15914  assapropd  16067  psrval  16110  prmirredlem  16446  lsmcss  16592  pptbas  16745  toponmre  16830  restbas  16889  iscncl  16998  cnrest2  17014  cnpdis  17021  lmcnp  17032  dishaus  17110  cmpcovf  17118  tgcmp  17128  dfcon2  17145  clscon  17156  2ndcctbss  17181  dis2ndc  17186  1stccnp  17188  islly2  17210  cldllycmp  17221  kgentopon  17233  txcls  17299  ptpjopn  17306  dfac14  17312  xkoccn  17313  txcnp  17314  txcmpb  17338  txlm  17342  xkopt  17349  xkoco1cn  17351  xkoco2cn  17352  qtopcn  17405  qtoprest  17408  regr1lem2  17431  xkocnv  17505  qtophmeo  17508  fmfnfmlem4  17652  hausflim  17676  hauspwpwf1  17682  fclscmp  17725  alexsublem  17738  alexsubALTlem2  17742  alexsubALTlem3  17743  ptcmplem3  17748  ptcmplem4  17749  ptcmplem5  17750  tmdgsum2  17779  symgtgp  17784  tsmsval2  17812  tsmsgsum  17821  ismet2  17898  blin  17970  metss2lem  18057  methaus  18066  met1stc  18067  met2ndci  18068  prdsxmslem2  18075  metcnp3  18086  metcnpi3  18092  nlmvscn  18198  nrginvrcn  18202  xrsxmet  18315  reconnlem1  18331  reconn  18333  xrge0tsms  18339  xmetdcn2  18342  metdscn  18360  addcnlem  18368  fsumcn  18374  cnheiborlem  18452  cnheibor  18453  bndth  18456  lebnum  18462  nmoleub2lem2  18597  ipcn  18673  iscmet3  18719  caubl  18733  minveclem3b  18792  minveclem7  18799  pjthlem2  18802  pmltpc  18810  volfiniun  18904  ioombl1  18919  dyadss  18949  dyaddisjlem  18950  dyadmax  18953  dyadmbllem  18954  opnmbllem  18956  itg1addlem2  19052  itg10a  19065  mbfi1fseqlem6  19075  itg2seq  19097  itg2monolem1  19105  itg2gt0  19115  itgfsum  19181  limcfval  19222  ellimc2  19227  ellimc3  19229  limcres  19236  limciun  19244  dvres  19261  dveflem  19326  rolle  19337  dvlip2  19342  c1liplem1  19343  dvgt0lem1  19349  dvgt0  19351  dvlt0  19352  dvne0  19358  dvfsumrlimge0  19377  ftc1lem6  19388  itgsubst  19396  evlslem1  19399  mdegmullem  19464  ply1domn  19509  ply1divex  19522  fta1g  19553  fta1b  19555  plyf  19580  dgrlem  19611  coeid  19620  plydivalg  19679  aannenlem1  19708  aalioulem3  19714  aalioulem6  19717  abelthlem8  19815  efif1olem4  19907  chordthm  20134  xrlimcnp  20263  jensen  20283  sqf11  20377  fsumvma2  20453  perfectlem2  20469  lgsdilem  20561  lgsquad2lem2  20598  lgsquad3  20600  2sqlem5  20607  2sqlem9  20612  2sqb  20617  rpvmasumlem  20636  dchrisum0flb  20659  dchrisum0  20669  pntpbnd  20737  pntibndlem3  20741  pntleml  20760  vacn  21267  blocni  21383  ubthlem3  21451  minvecolem7  21462  chocunii  21880  pjhthmo  21881  pjhthlem2  21971  kbass5  22700  mdsymlem5  22987  ballotlemfc0  23051  ballotlemfcc  23052  xrofsup  23255  gsumpropd2lem  23379  xrge0tsmsd  23382  derangenlem  23702  erdsze2lem1  23734  pconcon  23762  conpcon  23766  cvxscon  23774  cvmliftmolem2  23813  cvmliftmo  23815  cvmlift2lem10  23843  cvmlift2lem12  23845  cvmlift3lem7  23856  eupath2  23904  dedekind  24082  poseq  24253  brcgr  24528  brbtwn2  24533  colinearalg  24538  axsegcon  24555  axeuclidlem  24590  axcontlem9  24600  ifscgr  24667  cgrxfr  24678  btwnconn1lem13  24722  btwnconn1lem14  24723  outsideofeq  24753  ellines  24775  muldisc  25481  trnij  25615  icccon2  25700  imonclem  25813  idmon  25817  pdiveql  26168  finminlem  26231  locfincmp  26304  comppfsc  26307  fnejoin2  26318  upixp  26403  filbcmb  26432  sstotbnd2  26498  isbnd3  26508  prdsbnd2  26519  cntotbnd  26520  ismtyima  26527  bfp  26548  rrncmslem  26556  unichnidl  26656  nacsfix  26787  mzpsubst  26826  mzpcompact2lem  26829  eldioph2lem2  26840  eldioph2  26841  eldioph2b  26842  diophin  26852  diophun  26853  irrapxlem3  26909  irrapxlem5  26911  pell1234qrreccl  26939  pell1234qrmulcl  26940  pell14qrdich  26954  pell1qrge1  26955  pell1qrgaplem  26958  monotuz  27026  rpexpmord  27033  acongtr  27065  acongrep  27067  jm2.23  27089  jm2.26a  27093  jm2.26lem3  27094  jm2.26  27095  jm2.27  27101  wepwsolem  27138  fnwe2lem2  27148  kelac1  27161  kercvrlsm  27181  uvcf1  27241  frlmsslsp  27248  frlmup1  27250  hbtlem5  27332  hbt  27334  mpaaeu  27355  f1otrspeq  27390  psgneu  27429  mamucl  27456  mamulid  27458  mamurid  27459  mamuass  27460  mamudi  27461  mamudir  27462  mamuvs1  27463  mamuvs2  27464  cncmpmax  27703  rfcnnnub  27707  stoweidlem27  27776  stoweidlem31  27780  stoweidlem34  27783  stoweidlem35  27784  stoweidlem49  27798  stoweidlem59  27808  stoweidlem62  27811  lshpcmp  29178  islshpat  29207  lfl0f  29259  ishlat3N  29544  3dim1  29656  islvol5  29768  lvoli2  29770  lncvrelatN  29970  pclfinclN  30139  pexmidlem8N  30166  idltrn  30339  cdleme42keg  30675  cdleme42mgN  30677  cdlemf2  30751  cdlemg2cex  30780  trlcoat  30912  dihopelvalcpre  31438  dih1dimatlem  31519  dihjatcclem4  31611  lcfl7N  31691  lcfrlem9  31740  mapdh9a  31980  hdmapglem7  32122
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