MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simplrl 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  2647  rmob  3209  disjxiun  4169  f1imass  5969  soisoi  6007  riota5f  6533  tfrlem9a  6606  oeeui  6804  oaabs2  6847  omabs  6849  omxpenlem  7168  fopwdom  7175  frfi  7311  marypha1lem  7396  ordiso2  7440  oismo  7465  wemaplem3  7473  cantnf  7605  isinffi  7835  dfac12lem2  7980  dfac12lem3  7981  infxp  8051  infmap2  8054  infpssrlem5  8143  fin23lem11  8153  fin23lem24  8158  fin23lem26  8161  isf32lem2  8190  isf32lem4  8192  fin1a2lem13  8248  fin1a2s  8250  ttukeylem5  8349  fpwwe2lem12  8472  fpwwe2lem13  8473  wunex2  8569  tskord  8611  prlem934  8866  addid1  9202  cnegex  9203  negeu  9252  add20  9496  divdivdiv  9671  ltmul12a  9822  lediv12a  9859  cru  9948  uzwo3  10525  xleadd1a  10788  xlemul1a  10823  ixxun  10888  ixxss12  10892  mulexpz  11375  leexp1a  11393  expmulnbnd  11466  abs3lem  12097  rexanre  12105  cau3lem  12113  lo1bdd2  12273  o1lo1  12286  rlimclim1  12294  rlimclim  12295  lo1resb  12313  o1resb  12315  rlimcn2  12339  o1of2  12361  o1rlimmul  12367  lo1add  12375  lo1mul  12376  isercolllem1  12413  climcau  12419  summolem2  12465  summo  12466  o1fsum  12547  qredeu  13062  isprm5  13067  pclem  13167  pcqmul  13182  pcexp  13188  pcneg  13202  pcprmpw2  13210  pcadd  13213  prmpwdvds  13227  4sqlem13  13280  vdwlem2  13305  vdwlem7  13310  vdwlem11  13314  vdwlem12  13315  ramval  13331  ramz2  13347  ramcl  13352  imasval  13692  imasdsval  13696  mreexexd  13828  issubc3  14001  idfucl  14033  funcres2c  14053  fucpropd  14129  xpcval  14229  prfval  14251  evlfcl  14274  curf12  14279  curf1cl  14280  curf2  14281  curfcl  14284  curfuncf  14290  curf2ndf  14299  hof2val  14308  hofcl  14311  hofpropd  14319  yonedalem4a  14327  yonedainv  14333  poslubmo  14528  isipodrs  14542  acsmapd  14559  acsinfd  14561  mndpropd  14676  mhmeql  14719  frmdup3  14766  issubg4  14916  ssnmz  14937  sylow2blem3  15211  lsmdisj2  15269  pj1eu  15283  efgredlem  15334  frgpuplem  15359  frgpnabl  15441  dmdprdsplitlem  15550  pgpfac1lem3  15590  pgpfaclem3  15596  rngpropd  15650  dvdsrtr  15712  islmhm2  16069  lmhmpropd  16100  assapropd  16341  coe1tmmul2  16623  prmirredlem  16728  lsmcss  16874  toponmre  17112  restbas  17176  iscncl  17287  cnpdis  17311  lmcnp  17322  dishaus  17400  cmpcovf  17408  hauscmplem  17423  dfcon2  17435  clscon  17446  2ndcctbss  17471  1stccnp  17478  islly2  17500  llyidm  17504  cldllycmp  17511  kgentopon  17523  1stckgenlem  17538  ptpjpre1  17556  ptbasfi  17566  txcls  17589  ptpjopn  17597  xkoccn  17604  txcnp  17605  txcmpb  17629  xkoptsub  17639  xkoco2cn  17643  xkoinjcn  17672  qtopcn  17699  qtoprest  17702  regr1lem  17724  regr1lem2  17725  kqreglem1  17726  qtophmeo  17802  fgabs  17864  hauspwpwf1  17972  flimfnfcls  18013  fclscmp  18015  cnpfcf  18026  ptcmplem4  18039  ptcmplem5  18040  cnextfval  18046  cnextfun  18048  tmdgsum2  18079  tsmsval2  18112  utoptop  18217  utop3cls  18234  ismet2  18316  blin  18404  metss2lem  18494  methaus  18503  met1stc  18504  met2ndci  18505  metcnp  18524  metcnpi3  18529  metusttoOLD  18540  metustto  18541  metustfbasOLD  18548  metustfbas  18549  nlmvscn  18676  nrginvrcn  18680  nghmcn  18732  xrsxmet  18793  reconnlem1  18810  reconn  18812  xrge0tsms  18818  xmetdcn2  18821  metdscn  18839  addcnlem  18847  mulc1cncf  18888  cncfco  18890  cnheiborlem  18932  cnheibor  18933  nmoleub2lem2  19077  ipcn  19153  iscfil3  19179  cfilfcls  19180  iscmet3  19199  caubl  19213  bcthlem5  19234  minveclem3b  19282  minveclem7  19289  pmltpc  19300  ovolshftlem1  19358  ovolscalem1  19362  ioombl1  19409  uniioombllem6  19433  dyadss  19439  dyaddisjlem  19440  dyadmax  19443  opnmbllem  19446  itg1addlem2  19542  itg2seq  19587  bddmulibl  19683  limcfval  19712  ellimc3  19719  limciun  19734  dveflem  19816  rolle  19827  dvlip2  19832  c1liplem1  19833  dvgt0lem1  19839  dvgt0  19841  dvlt0  19842  dvne0  19848  dvcnvre  19856  dvfsumrlimge0  19867  ftc1lem6  19878  itgsubst  19886  evlslem1  19889  mdegmullem  19954  ply1domn  19999  fta1g  20043  fta1b  20045  dgrlem  20101  coeid  20110  plydivalg  20169  aannenlem1  20198  aalioulem6  20207  ulmcn  20268  mtestbdd  20274  abelthlem8  20308  efif1olem4  20400  chordthm  20631  xrlimcnp  20760  isppw2  20851  fsumvma2  20951  perfectlem2  20967  lgsdilem  21059  lgsquad2lem2  21096  lgsquad3  21098  2sqlem5  21105  2sqlem9  21110  rpvmasumlem  21134  dchrisum0flb  21157  pntpbnd  21235  pntibndlem3  21239  pntlem3  21256  pntleml  21258  usgrasscusgra  21445  4cycl4dv4e  21608  eupath2  21655  vacn  22143  ubthlem1  22325  ubthlem3  22327  minvecolem7  22338  chocunii  22756  pjhthmo  22757  pjhthlem2  22847  nmopub2tALT  23365  nmfnleub2  23382  kbass5  23576  mdslmd1lem1  23781  mdslmd1lem2  23782  mdsymlem5  23863  xrofsup  24079  xrge0tsmsd  24176  qqhval2  24319  esumpcvgval  24421  imambfm  24565  ballotlemsf1o  24724  lgamgulmlem5  24770  pconcon  24871  conpcon  24875  cvmliftmo  24924  cvmlift2lem10  24952  cvmlift2lem12  24954  cvmlift3lem7  24965  dedekind  25140  prodmolem2  25214  axsegcon  25770  axpasch  25784  axeuclidlem  25805  ifscgr  25882  cgrxfr  25893  btwnconn1lem13  25937  ellines  25990  mblfinlem  26143  mblfinlem2  26144  itg2addnclem  26155  itg2addnc  26158  ftc1cnnc  26178  locfincmp  26274  sstotbnd  26374  cntotbnd  26395  ismtyima  26402  heibor1lem  26408  heiborlem10  26419  bfp  26423  rrncmslem  26431  isnacs3  26654  nacsfix  26656  mzpsubst  26695  eldioph2lem2  26709  eldioph2  26710  eldioph2b  26711  diophin  26721  diophun  26722  rencldnfilem  26771  irrapxlem3  26777  irrapxlem5  26779  pell1234qrreccl  26807  pell1234qrmulcl  26808  pell1qrge1  26823  pell1qrgaplem  26826  monotuz  26894  monotoddzzfi  26895  rpexpmord  26901  acongtr  26933  acongrep  26935  jm2.26a  26961  jm2.26lem3  26962  jm2.26  26963  jm2.27b  26967  jm2.27  26969  wepwsolem  27006  fnwe2lem2  27016  dsmmlss  27078  uvcf1  27109  frlmup1  27118  hbtlem5  27200  hbt  27202  mpaaeu  27223  f1otrspeq  27258  psgneu  27297  mamucl  27324  mamulid  27326  mamurid  27327  mamuass  27328  mamudi  27329  mamudir  27330  mamuvs1  27331  mamuvs2  27332  fnchoice  27567  rfcnnnub  27574  stoweidlem14  27630  stoweidlem27  27643  stoweidlem34  27650  stoweidlem49  27665  stoweidlem56  27672  elfzelfzelfz  27981  swrdccat3  28029  usg2spthonot1  28087  usg2spot2nb  28168  islshpsm  29463  lsatcmp  29486  islshpat  29500  lfl0f  29552  iscvlat2N  29807  ishlat3N  29837  3dim1  29949  islvol5  30061  lvoli2  30063  lncvrelatN  30263  lncmp  30265  paddasslem10  30311  pclfinclN  30432  pexmidlem8N  30459  idltrn  30632  cdleme42keg  30968  cdleme42mgN  30970  cdlemf2  31044  cdlemg2cex  31073  trlcoat  31205  tendoex  31457  erngdvlem4  31473  erngdvlem4-rN  31481  dialss  31529  dibglbN  31649  diblss  31653  dihlsscpre  31717  dihglblem2aN  31776  dihglblem4  31780  dihglblem5  31781  dih1dimatlem  31812  dihglblem6  31823  lcfl7N  31984  lcfrlem9  32033  mapdh9a  32273  hdmapglem7  32415
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