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

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

Proof of Theorem simplrl
StepHypRef Expression
1 simpl 444 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antlr 708 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  pm2.61da3ne  2678  rmob  3241  disjxiun  4201  f1imass  6002  soisoi  6040  riota5f  6566  tfrlem9a  6639  oeeui  6837  oaabs2  6880  omabs  6882  omxpenlem  7201  fopwdom  7208  frfi  7344  marypha1lem  7430  ordiso2  7476  oismo  7501  wemaplem3  7509  cantnf  7641  isinffi  7871  dfac12lem2  8016  dfac12lem3  8017  infxp  8087  infmap2  8090  infpssrlem5  8179  fin23lem11  8189  fin23lem24  8194  fin23lem26  8197  isf32lem2  8226  isf32lem4  8228  fin1a2lem13  8284  fin1a2s  8286  ttukeylem5  8385  fpwwe2lem12  8508  fpwwe2lem13  8509  wunex2  8605  tskord  8647  prlem934  8902  addid1  9238  cnegex  9239  negeu  9288  add20  9532  divdivdiv  9707  ltmul12a  9858  lediv12a  9895  cru  9984  uzwo3  10561  xleadd1a  10824  xlemul1a  10859  ixxun  10924  ixxss12  10928  mulexpz  11412  leexp1a  11430  expmulnbnd  11503  abs3lem  12134  rexanre  12142  cau3lem  12150  lo1bdd2  12310  o1lo1  12323  rlimclim1  12331  rlimclim  12332  lo1resb  12350  o1resb  12352  rlimcn2  12376  o1of2  12398  o1rlimmul  12404  lo1add  12412  lo1mul  12413  isercolllem1  12450  climcau  12456  summolem2  12502  summo  12503  o1fsum  12584  qredeu  13099  isprm5  13104  pclem  13204  pcqmul  13219  pcexp  13225  pcneg  13239  pcprmpw2  13247  pcadd  13250  prmpwdvds  13264  4sqlem13  13317  vdwlem2  13342  vdwlem7  13347  vdwlem11  13351  vdwlem12  13352  ramval  13368  ramz2  13384  ramcl  13389  imasval  13729  imasdsval  13733  mreexexd  13865  issubc3  14038  idfucl  14070  funcres2c  14090  fucpropd  14166  xpcval  14266  prfval  14288  evlfcl  14311  curf12  14316  curf1cl  14317  curf2  14318  curfcl  14321  curfuncf  14327  curf2ndf  14336  hof2val  14345  hofcl  14348  hofpropd  14356  yonedalem4a  14364  yonedainv  14370  poslubmo  14565  isipodrs  14579  acsmapd  14596  acsinfd  14598  mndpropd  14713  mhmeql  14756  frmdup3  14803  issubg4  14953  ssnmz  14974  sylow2blem3  15248  lsmdisj2  15306  pj1eu  15320  efgredlem  15371  frgpuplem  15396  frgpnabl  15478  dmdprdsplitlem  15587  pgpfac1lem3  15627  pgpfaclem3  15633  rngpropd  15687  dvdsrtr  15749  islmhm2  16106  lmhmpropd  16137  assapropd  16378  coe1tmmul2  16660  prmirredlem  16765  lsmcss  16911  toponmre  17149  restbas  17214  iscncl  17325  cnpdis  17349  lmcnp  17360  dishaus  17438  cmpcovf  17446  hauscmplem  17461  dfcon2  17474  clscon  17485  2ndcctbss  17510  1stccnp  17517  islly2  17539  llyidm  17543  cldllycmp  17550  kgentopon  17562  1stckgenlem  17577  ptpjpre1  17595  ptbasfi  17605  txcls  17628  ptpjopn  17636  xkoccn  17643  txcnp  17644  txcmpb  17668  xkoptsub  17678  xkoco2cn  17682  xkoinjcn  17711  qtopcn  17738  qtoprest  17741  regr1lem  17763  regr1lem2  17764  kqreglem1  17765  qtophmeo  17841  fgabs  17903  hauspwpwf1  18011  flimfnfcls  18052  fclscmp  18054  cnpfcf  18065  ptcmplem4  18078  ptcmplem5  18079  cnextfval  18085  cnextfun  18087  tmdgsum2  18118  tsmsval2  18151  utoptop  18256  utop3cls  18273  ismet2  18355  blin  18443  metss2lem  18533  methaus  18542  met1stc  18543  met2ndci  18544  metcnp  18563  metcnpi3  18568  metusttoOLD  18579  metustto  18580  metustfbasOLD  18587  metustfbas  18588  nlmvscn  18715  nrginvrcn  18719  nghmcn  18771  xrsxmet  18832  reconnlem1  18849  reconn  18851  xrge0tsms  18857  xmetdcn2  18860  metdscn  18878  addcnlem  18886  mulc1cncf  18927  cncfco  18929  cnheiborlem  18971  cnheibor  18972  nmoleub2lem2  19116  ipcn  19192  iscfil3  19218  cfilfcls  19219  iscmet3  19238  caubl  19252  bcthlem5  19273  minveclem3b  19321  minveclem7  19328  pmltpc  19339  ovolshftlem1  19397  ovolscalem1  19401  ioombl1  19448  uniioombllem6  19472  dyadss  19478  dyaddisjlem  19479  dyadmax  19482  opnmbllem  19485  itg1addlem2  19581  itg2seq  19626  bddmulibl  19722  limcfval  19751  ellimc3  19758  limciun  19773  dveflem  19855  rolle  19866  dvlip2  19871  c1liplem1  19872  dvgt0lem1  19878  dvgt0  19880  dvlt0  19881  dvne0  19887  dvcnvre  19895  dvfsumrlimge0  19906  ftc1lem6  19917  itgsubst  19925  evlslem1  19928  mdegmullem  19993  ply1domn  20038  fta1g  20082  fta1b  20084  dgrlem  20140  coeid  20149  plydivalg  20208  aannenlem1  20237  aalioulem6  20246  ulmcn  20307  mtestbdd  20313  abelthlem8  20347  efif1olem4  20439  chordthm  20670  xrlimcnp  20799  isppw2  20890  fsumvma2  20990  perfectlem2  21006  lgsdilem  21098  lgsquad2lem2  21135  lgsquad3  21137  2sqlem5  21144  2sqlem9  21149  rpvmasumlem  21173  dchrisum0flb  21196  pntpbnd  21274  pntibndlem3  21278  pntlem3  21295  pntleml  21297  usgrasscusgra  21484  4cycl4dv4e  21647  eupath2  21694  vacn  22182  ubthlem1  22364  ubthlem3  22366  minvecolem7  22377  chocunii  22795  pjhthmo  22796  pjhthlem2  22886  nmopub2tALT  23404  nmfnleub2  23421  kbass5  23615  mdslmd1lem1  23820  mdslmd1lem2  23821  mdsymlem5  23902  xrofsup  24118  xrge0tsmsd  24215  qqhval2  24358  esumpcvgval  24460  imambfm  24604  ballotlemsf1o  24763  lgamgulmlem5  24809  pconcon  24910  conpcon  24914  cvmliftmo  24963  cvmlift2lem10  24991  cvmlift2lem12  24993  cvmlift3lem7  25004  dedekind  25179  prodmolem2  25253  axsegcon  25858  axpasch  25872  axeuclidlem  25893  ifscgr  25970  cgrxfr  25981  btwnconn1lem13  26025  ellines  26078  mblfinlem  26234  mblfinlem2  26235  itg2addnclem  26246  itg2addnc  26249  ftc1cnnc  26269  locfincmp  26375  sstotbnd  26475  cntotbnd  26496  ismtyima  26503  heibor1lem  26509  heiborlem10  26520  bfp  26524  rrncmslem  26532  isnacs3  26755  nacsfix  26757  mzpsubst  26796  eldioph2lem2  26810  eldioph2  26811  eldioph2b  26812  diophin  26822  diophun  26823  rencldnfilem  26872  irrapxlem3  26878  irrapxlem5  26880  pell1234qrreccl  26908  pell1234qrmulcl  26909  pell1qrge1  26924  pell1qrgaplem  26927  monotuz  26995  monotoddzzfi  26996  rpexpmord  27002  acongtr  27034  acongrep  27036  jm2.26a  27062  jm2.26lem3  27063  jm2.26  27064  jm2.27b  27068  jm2.27  27070  wepwsolem  27107  fnwe2lem2  27117  dsmmlss  27178  uvcf1  27209  frlmup1  27218  hbtlem5  27300  hbt  27302  mpaaeu  27323  f1otrspeq  27358  psgneu  27397  mamucl  27424  mamulid  27426  mamurid  27427  mamuass  27428  mamudi  27429  mamudir  27430  mamuvs1  27431  mamuvs2  27432  fnchoice  27667  rfcnnnub  27674  stoweidlem14  27730  stoweidlem27  27743  stoweidlem34  27750  stoweidlem49  27765  stoweidlem56  27772  elfzelfzelfz  28093  cshweqdif2s  28234  cshwssizelem4a  28246  usg2spthonot1  28310  usg2spot2nb  28391  islshpsm  29715  lsatcmp  29738  islshpat  29752  lfl0f  29804  iscvlat2N  30059  ishlat3N  30089  3dim1  30201  islvol5  30313  lvoli2  30315  lncvrelatN  30515  lncmp  30517  paddasslem10  30563  pclfinclN  30684  pexmidlem8N  30711  idltrn  30884  cdleme42keg  31220  cdleme42mgN  31222  cdlemf2  31296  cdlemg2cex  31325  trlcoat  31457  tendoex  31709  erngdvlem4  31725  erngdvlem4-rN  31733  dialss  31781  dibglbN  31901  diblss  31905  dihlsscpre  31969  dihglblem2aN  32028  dihglblem4  32032  dihglblem5  32033  dih1dimatlem  32064  dihglblem6  32075  lcfl7N  32236  lcfrlem9  32285  mapdh9a  32525  hdmapglem7  32667
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