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

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

Proof of Theorem simpllr
StepHypRef Expression
1 simpr 458 . 2  |-  ( (
ph  /\  ps )  ->  ps )
21ad2antrr 718 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ps )
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:  simp-4r  759  soisoi  6006  f1o2ndf1  6669  tfrlem1  6821  tz7.49  6886  omabs  7074  omxpenlem  7400  fopwdom  7407  findcard3  7543  frfi  7545  finsschain  7606  marypha1lem  7671  wdomtr  7778  cantnfp1  7877  cantnfp1OLD  7903  harcard  8136  numacn  8207  infunsdom1  8370  cofsmo  8426  sornom  8434  ssfin4  8467  fin1a2lem11  8567  fin1a2lem13  8569  ttukeylem5  8670  fpwwe2lem13  8797  pwfseq  8819  00id  9532  addid1  9537  cnegex  9538  negeu  9588  add20  9839  ltmul12a  10173  lediv12a  10213  cru  10302  qextltlem  11160  xleadd1a  11204  xmullem  11215  xlemul1a  11239  ixxss12  11308  ioodisj  11402  seqf1o  11831  mulexpz  11888  leexp1a  11906  faclbnd  12050  swrdswrdlem  12337  abs3lem  12810  cau3lem  12826  rlim3  12960  ello12  12978  lo1bdd2  12986  elo12  12989  rlimconst  13006  isercoll  13129  climcau  13132  climbdd  13133  summolem2  13177  fsumconst  13240  o1fsum  13259  incexclem  13282  bitsfzo  13614  dvdsmulgcd  13721  pc2dvds  13928  pcz  13930  pcadd  13934  pcfac  13944  vdwmc2  14023  vdwlem2  14026  vdwlem10  14034  vdw  14038  ramcl  14073  sbcie3s  14201  firest  14354  prdsval  14376  mreexd  14563  mreexexlemd  14565  iscat  14593  cidfval  14597  iscatd2  14602  catcocl  14606  catass  14607  catpropd  14631  cidpropd  14632  moni  14658  monpropd  14659  issubc  14731  subccocl  14738  funcco  14764  funcpropd  14793  fullpropd  14813  nati  14848  natpropd  14869  fucpropd  14870  xpcpropd  15001  curfuncf  15031  curf2ndf  15040  yonffthlem  15075  acsfiindd  15330  mndpropd  15429  mhmeql  15474  isgrpinv  15568  conjnmzb  15761  gass  15799  symgextf  15902  dfod2  16045  gexdvds  16063  sylow3lem2  16107  efgredlem  16224  efgredeu  16229  oddvdssubg  16317  dprdfcntz  16473  dprdfcntzOLD  16479  pgpfaclem3  16558  isrng  16585  dvdsrmul1  16679  issubdrg  16814  islmhm2  17041  lmhmeql  17058  lssacsex  17147  issubassa2  17337  opsrval  17488  isphl  17899  uvcf1  18059  lindfmm  18098  mdetunilem7  18266  gsummatr01lem4  18306  cctop  18452  neiptoptop  18577  neiptopreu  18579  tgrest  18605  ordtrest2lem  18649  cnss1  18722  cncnp  18726  isnrm3  18805  uncmp  18848  cmpfi  18853  iuncon  18874  1stcrest  18899  subislly  18927  islly2  18930  cldllycmp  18941  lly1stc  18942  llycmpkgen2  18965  kgencn  18971  xkoccn  19034  ptcnplem  19036  pthaus  19053  txhaus  19062  txkgen  19067  xkohaus  19068  xkococnlem  19074  txcon  19104  regr1lem2  19155  kqreglem1  19156  reghmph  19208  nrmhmph  19209  trfil2  19302  ufileu  19334  flimopn  19390  flimcf  19397  fclscf  19440  ufilcmp  19447  cnpfcf  19456  cnextfun  19478  tgpmulg  19506  symgtgp  19514  tgpt0  19531  divstgplem  19533  ustex2sym  19633  ustex3sym  19634  trust  19646  restutop  19654  restutopopn  19655  ustuqtop2  19659  ustuqtop4  19661  utop3cls  19668  utopreg  19669  cstucnd  19701  ucncn  19702  trcfilu  19711  neipcfilu  19713  ismet2  19750  metequiv2  19927  metcnp  19958  metcnp2  19959  metcnpi3  19963  txmetcnp  19964  metusttoOLD  19974  metustto  19975  metustsymOLD  19978  metustsym  19979  metustOLD  19984  metust  19985  cfilucfilOLD  19986  cfilucfil  19987  metuel2  19996  metutopOLD  19999  psmetutop  20000  restmetu  20004  metucnOLD  20005  metucn  20006  ngptgp  20064  tngngp  20082  nmoleub  20152  icccmp  20244  reconnlem2  20246  reconn  20247  xmetdcn2  20256  metdseq0  20272  metdscn  20274  elcncf2  20308  cncfmet  20326  cnheibor  20369  nmoleub2lem2  20513  nmoleub3  20516  iscfil2  20619  iscfil3  20626  cfilfcls  20627  equivcfil  20652  caubl  20660  bcthlem5  20681  pmltpc  20776  ovollb2  20814  ovoliunnul  20832  ovolicc2lem4  20845  volsup  20879  ioorf  20895  dyadss  20916  dyaddisjlem  20917  mbfposr  20972  cncombf  20978  mbflimsup  20986  i1fmulclem  21022  mbfi1fseqlem4  21038  iblss2  21125  ellimc2  21194  ellimc3  21196  dvnadd  21245  dvmptfsum  21289  dvferm1  21299  dvferm2  21301  fta1g  21524  plyeq0lem  21563  plydivex  21648  fta1  21659  aalioulem2  21684  aalioulem3  21685  ulmuni  21742  ulmbdd  21748  ulmdvlem3  21752  mtest  21754  abelthlem8  21789  pilem3  21803  efopn  21988  cxpmul2z  22021  cxpcn3lem  22070  jensen  22267  isppw2  22338  sqf11  22362  mersenne  22451  dchrelbas3  22462  dchrptlem1  22488  dchrpt  22491  lgsval2lem  22530  lgsdchrval  22571  lgsquad3  22585  2sqb  22602  pntrsumbnd2  22701  pntpbnd  22722  pntibnd  22727  istrkgc  22802  istrkgb  22803  tglowdim1i  22836  tgbtwndiff  22841  tgifscgr  22842  tgcgrxfr  22851  lnext  22875  tgbtwnconn1lem3  22882  tgbtwnconn1  22883  legval  22891  legov  22892  legov2  22893  legtrd  22896  legtri3  22897  tglinethru  22913  colline  22918  tglowdim2l  22919  mirreu3  22924  miriso  22935  f1otrg  22940  f1otrge  22941  axsegcon  22996  axeuclidlem  23031  axcontlem2  23034  usgra1  23115  usgrares1  23146  nbgraf1olem5  23177  pthdepisspth  23296  iseupa  23409  eupath2  23424  isgrp2d  23545  smcnlem  23915  0lno  24013  ubthlem1  24094  ubthlem3  24096  chocunii  24527  occl  24530  5oalem1  24880  3oalem2  24889  nmopub2tALT  25136  nmfnleub2  25153  lnconi  25260  kbass5  25347  mdslmd1lem1  25552  mdslmd1lem2  25553  cdj1i  25660  disjabrex  25750  disjabrexf  25751  fgreu  25814  xrofsup  25878  ressprs  25939  xrge0addgt0  25977  submarchi  26027  isarchi3  26028  archiabllem1  26034  archiabllem2a  26035  issrg  26042  gsumle  26098  suborng  26136  isarchiofld  26138  pstmxmet  26178  sqsscirc1  26192  ordtrest2NEWlem  26206  ordtconlem1  26208  pnfneige0  26235  lmxrge0  26236  lmdvg  26237  qqhval2  26265  esumcst  26368  esumfsup  26373  esumcvg  26389  sigaclfu2  26418  insiga  26434  measinb  26489  imambfm  26531  eulerpartlemgvv  26607  dstrvprob  26702  sgnmul  26773  sgnsub  26775  signstfvneq0  26821  afsval  26843  lgambdd  26871  lgamucov  26872  derangenlem  26907  sconpi1  26976  cvmsss2  27011  cvmopnlem  27015  cvmlift3lem7  27062  fprodconst  27336  ifscgr  27922  cgrxfr  27933  btwnconn1lem13  27977  outsideofeu  28009  heicant  28270  mblfinlem1  28272  itg2addnclem  28287  ftc1cnnc  28310  ftc1anclem7  28317  neibastop2lem  28425  sstotbnd2  28517  equivtotbnd  28521  isbnd3  28527  ssbnd  28531  totbndbnd  28532  cntotbnd  28539  heibor1lem  28552  rrncmslem  28575  mzpindd  28927  mzpsubst  28930  mzpcompact2lem  28933  eldioph2b  28946  irrapxlem3  29010  irrapxlem5  29012  pellex  29021  pell1234qrdich  29047  pell14qrexpcl  29053  congabseq  29162  jm2.26a  29194  jm2.26lem3  29195  rmydioph  29208  lnrfg  29320  hbt  29331  fnchoice  29596  cncmpmax  29599  climrec  29622  climsuse  29627  stoweidlem7  29648  stoweidlem34  29675  stoweidlem52  29693  stoweidlem60  29701  wallispilem3  29708  usgra2pthspth  30141  el2spthonot  30235  usg2wotspth  30249  clwwlkf1  30304  Lemma2  30339  frgrancvvdeqlem9  30480  friendshipgt3  30560  lindslinindsimp2  30706  snlindsntor  30714  lincresunit2  30721  islindeps2  30726  4animp1  30902  4an4132  30904  iunconlem2  31373  lssats  32230  lsat0cv  32251  lkrlss  32313  lfl1dim  32339  lfl1dim2N  32340  lkrpssN  32381  hlhgt2  32606  3dim2  32685  2dim  32687  lplncvrlvol  32833  paddasslem11  33047  pmapjat1  33070  2polssN  33132  pclfinclN  33167  pexmidlem8N  33194  lhpexle1lem  33224  4atex  33293  ltrnid  33352  trlator0  33388  cdlemg2cex  33808  tendodi1  34001  tendodi2  34002  diblss  34388  dihopelvalcpre  34466  dihatexv  34556  mapdval4N  34850
  Copyright terms: Public domain W3C validator