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

Theorem simplrr 760
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 461 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antlr 726 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  pm2.61da3neOLD  2788  rmob  3431  disjxiun  4444  isotr  6218  weniso  6236  riota5f  6268  tfrlem9a  7052  oaass  7207  oeeui  7248  oaabs2  7291  resixpfo  7504  omxpenlem  7615  pw2f1olem  7618  fopwdom  7622  fofinf1o  7797  marypha1lem  7889  ordiso2  7936  oismo  7961  ixpiunwdom  8013  cantnf  8108  cantnfOLD  8130  fseqenlem1  8401  iunfictbso  8491  dfac12lem2  8520  dfac12lem3  8521  infunsdom1  8589  infpssrlem5  8683  fin23lem24  8698  isf32lem2  8730  isf32lem4  8732  isf34lem4  8753  fin1a2lem12  8787  fin1a2lem13  8788  ttukeylem6  8890  fpwwe2lem12  9015  fpwwe2lem13  9016  fpwwe2  9017  winalim2  9070  wunex2  9112  tskord  9154  prlem934  9407  mulcmpblnr  9444  dedekind  9739  addid1  9755  cnegex  9756  negeu  9806  add20  10060  divdivdiv  10241  ltmul12a  10394  lemul12a  10396  lediv12a  10434  supmul1  10504  cru  10524  uzwo3  11173  xleadd1a  11441  xmullem  11452  xmulgt0  11471  xlemul1a  11476  ixxun  11541  ixxss12  11545  ioodisj  11646  fz0fzelfz0  11774  mulexpz  12168  leexp1a  12186  expmulnbnd  12260  hashf1  12466  brfi1uzind  12492  reuccats1  12663  abs3lem  13127  rexanre  13135  cau3lem  13143  limsupgre  13260  limsupbnd2  13262  o1lo1  13316  rlimclim1  13324  rlimclim  13325  rlimcn1  13367  rlimcn2  13369  o1of2  13391  o1rlimmul  13397  lo1add  13405  lo1mul  13406  isercolllem1  13443  climcau  13449  caucvgrlem  13451  caucvgb  13458  summolem2  13494  summo  13495  modfsummod  13564  o1fsum  13583  isprm6  14102  isprm5  14105  rpdvds  14117  pclem  14214  pcqmul  14229  pcexp  14235  pcneg  14249  pcprmpw2  14257  pcadd  14260  pcmpt  14263  4sqlem13  14327  vdwlem2  14352  vdwlem7  14357  vdwlem12  14362  ramval  14378  ramub2  14384  ramz2  14394  ramcl  14399  cshwshashlem2  14432  imasval  14759  imasdsval  14763  mreexexd  14896  acsfn  14907  issubc3  15069  idfucl  15101  funcres2c  15121  isnat  15167  fucpropd  15197  xpcval  15297  xpcco  15303  prfval  15319  evlf2  15338  evlfcl  15342  curf12  15347  curf1cl  15348  curf2  15349  curfcl  15352  curf2ndf  15367  hof2val  15376  hofcl  15379  hofpropd  15387  yonedalem4a  15395  yonedainv  15401  drsdirfi  15418  pospo  15453  poslubmo  15626  posglbmo  15627  isipodrs  15641  acsinfd  15660  mndpropd  15756  mhmeql  15802  mrcmndind  15804  gsumvalx  15812  gsumpropd2lem  15815  frmdup3  15854  issubg4  16012  ssnmz  16035  conjnmzb  16093  f1otrspeq  16265  psgneu  16324  pgpfi  16418  sylow2blem3  16435  slwhash  16437  fislw  16438  sylow3lem2  16441  lsmdisj2  16493  pj1eu  16507  efgredlem  16558  frgpuplem  16583  gexex  16649  frgpnabl  16667  dprdfadd  16847  dprdfaddOLD  16854  dpjidcl  16894  dpjidclOLD  16901  pgpfac1lem3  16915  pgpfaclem3  16921  ablfac2  16927  rngpropd  17014  islmhm2  17464  lmhmpropd  17499  lbsextlem4  17587  assapropd  17744  psrval  17779  evlslem1  17952  prmirredlem  18287  prmirredlemOLD  18290  psgndiflemA  18401  lsmcss  18487  uvcf1  18587  frlmsslsp  18593  frlmsslspOLD  18594  frlmup1  18596  mamucl  18667  mamuass  18668  mamudi  18669  mamudir  18670  mamuvs1  18671  mamuvs2  18672  mamulid  18707  mamurid  18708  dmatsubcl  18764  dmatmulcl  18766  scmatscm  18779  marrepval  18828  marepveval  18834  mdetunilem7  18884  gsummatr01lem4  18924  cpmatmcllem  18983  mat2pmatf1  18994  mat2pmatlin  19000  decpmatmul  19037  pm2mpmhmlem2  19084  chpidmat  19112  pptbas  19272  toponmre  19357  restbas  19422  iscncl  19533  cnrest2  19550  cnpdis  19557  lmcnp  19568  dishaus  19646  cmpcovf  19654  tgcmp  19664  dfcon2  19683  clscon  19694  2ndcctbss  19719  dis2ndc  19724  1stccnp  19726  islly2  19748  cldllycmp  19759  kgentopon  19771  txcls  19837  ptpjopn  19845  dfac14  19851  xkoccn  19852  txcnp  19853  txcmpb  19877  txlm  19881  xkopt  19888  xkoco1cn  19890  xkoco2cn  19891  qtopcn  19947  qtoprest  19950  regr1lem2  19973  xkocnv  20047  qtophmeo  20050  fmfnfmlem4  20190  hausflim  20214  hauspwpwf1  20220  fclscmp  20263  alexsublem  20276  alexsubALTlem2  20280  alexsubALTlem3  20281  ptcmplem3  20286  ptcmplem4  20287  ptcmplem5  20288  cnextfun  20296  tmdgsum2  20327  symgtgp  20332  tsmsval2  20360  tsmsgsum  20369  tsmsgsumOLD  20372  utoptop  20469  ismet2  20568  blin  20656  metss2lem  20746  methaus  20755  met1stc  20756  met2ndci  20757  prdsxmslem2  20764  metcnp3  20775  metcnpi3  20781  metusttoOLD  20792  metustto  20793  metustfbasOLD  20800  metustfbas  20801  nlmvscn  20928  nrginvrcn  20932  xrsxmet  21046  reconnlem1  21063  reconn  21065  xrge0tsms  21071  xmetdcn2  21074  metdscn  21092  addcnlem  21100  fsumcn  21106  cnheiborlem  21186  cnheibor  21187  bndth  21190  lebnum  21196  nmoleub2lem2  21331  ipcn  21418  iscmet3  21464  caubl  21478  rrxdstprj1  21568  minveclem3b  21575  minveclem7  21582  pjthlem2  21585  pmltpc  21594  volfiniun  21689  ioombl1  21704  dyadss  21735  dyaddisjlem  21736  dyadmax  21739  dyadmbllem  21740  opnmbllem  21742  itg1addlem2  21836  itg10a  21849  mbfi1fseqlem6  21859  itg2seq  21881  itg2monolem1  21889  itg2gt0  21899  itgfsum  21965  limcfval  22008  ellimc2  22013  ellimc3  22015  limcres  22022  limciun  22030  dvres  22047  dveflem  22112  rolle  22123  dvlip2  22128  c1liplem1  22129  dvgt0lem1  22135  dvgt0  22137  dvlt0  22138  dvne0  22144  dvfsumrlimge0  22163  ftc1lem6  22174  itgsubst  22182  mdegmullem  22210  ply1domn  22256  ply1divex  22269  fta1g  22300  fta1b  22302  plyf  22327  dgrlem  22358  coeid  22367  plydivalg  22426  aannenlem1  22455  aalioulem3  22461  aalioulem6  22464  abelthlem8  22565  efif1olem4  22662  chordthm  22893  xrlimcnp  23023  jensen  23043  sqf11  23138  fsumvma2  23214  perfectlem2  23230  lgsdilem  23322  lgsquad2lem2  23359  lgsquad3  23361  2sqlem5  23368  2sqlem9  23373  2sqb  23378  rpvmasumlem  23397  dchrisum0flb  23420  dchrisum0  23430  pntpbnd  23498  pntibndlem3  23502  pntleml  23521  legov  23696  legtrid  23702  tglinethru  23727  tglnpt2  23731  tglineintmo  23732  mirreu3  23745  perpcom  23795  colperpexlem3  23808  mideulem  23810  mideu  23811  brcgr  23876  brbtwn2  23881  colinearalg  23886  axsegcon  23903  axeuclidlem  23938  axcontlem9  23948  ecgrtg  23959  elntg  23960  eengtrkg  23961  cusgrarn  24132  usgrasscusgra  24156  4cycl4dv4e  24341  wwlkext2clwwlk  24476  usg2spthonot1  24563  usgfidegfi  24583  eupath2  24653  usg2spot2nb  24739  numclwwlk6  24787  vacn  25277  blocni  25393  ubthlem3  25461  minvecolem7  25472  chocunii  25892  pjhthmo  25893  pjhthlem2  25983  kbass5  26712  mdsymlem5  26999  fcobij  27217  xrofsup  27247  archirngz  27392  archiabllem2a  27397  xrge0tsmsd  27435  isarchiofld  27467  qqhval2  27596  volmeas  27840  ballotlemfc0  28068  ballotlemfcc  28069  signstfvneq0  28166  lgamcvglem  28219  lgamcvg2  28234  derangenlem  28252  erdsze2lem1  28284  pconcon  28313  conpcon  28317  cvxscon  28325  cvmliftmolem2  28364  cvmliftmo  28366  cvmlift2lem10  28394  cvmlift2lem12  28396  cvmlift3lem7  28407  prodmolem2  28641  poseq  28907  ifscgr  29268  cgrxfr  29279  btwnconn1lem13  29323  btwnconn1lem14  29324  outsideofeq  29354  ellines  29376  supaddc  29615  opnmbllem0  29625  mblfinlem3  29628  itg2addnclem  29641  itg2addnc  29644  ftc1cnnc  29664  finminlem  29711  locfincmp  29774  comppfsc  29777  fnejoin2  29788  upixp  29821  filbcmb  29832  sstotbnd2  29871  isbnd3  29881  prdsbnd2  29892  cntotbnd  29893  ismtyima  29900  bfp  29921  rrncmslem  29929  unichnidl  30029  nacsfix  30246  mzpsubst  30283  mzpcompact2lem  30286  eldioph2lem2  30296  eldioph2  30297  eldioph2b  30298  diophin  30308  diophun  30309  irrapxlem3  30362  irrapxlem5  30364  pell1234qrreccl  30392  pell1234qrmulcl  30393  pell14qrdich  30407  pell1qrge1  30408  pell1qrgaplem  30411  monotuz  30479  rpexpmord  30486  acongtr  30518  acongrep  30520  jm2.23  30542  jm2.26a  30546  jm2.26lem3  30547  jm2.26  30548  jm2.27  30554  wepwsolem  30591  fnwe2lem2  30601  kelac1  30613  kercvrlsm  30633  hbtlem5  30681  hbt  30683  mpaaeu  30704  cncmpmax  30985  rfcnnnub  30989  iccintsng  31127  lptioo2  31173  lptioo1  31174  limclner  31193  stoweidlem31  31331  stoweidlem34  31334  stoweidlem35  31335  stoweidlem49  31349  stoweidlem59  31359  stoweidlem62  31362  fourierdlem42  31449  fourierdlem60  31467  fourierdlem61  31468  fourierdlem87  31494  usgedgvadf1lem2  31883  usgedgvadf1ALTlem2  31886  mndpsuppss  32037  scmsuppss  32038  lindslinindsimp2lem5  32136  lshpcmp  33785  islshpat  33814  lfl0f  33866  ishlat3N  34151  3dim1  34263  islvol5  34375  lvoli2  34377  lncvrelatN  34577  pclfinclN  34746  pexmidlem8N  34773  idltrn  34946  cdleme42keg  35282  cdleme42mgN  35284  cdlemf2  35358  cdlemg2cex  35387  trlcoat  35519  dihopelvalcpre  36045  dih1dimatlem  36126  dihjatcclem4  36218  lcfl7N  36298  lcfrlem9  36347  mapdh9a  36587  hdmapglem7  36729
  Copyright terms: Public domain W3C validator