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

Theorem simplrl 736
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 443 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antlr 707 1  |-  ( ( ( ph  /\  ( ps  /\  ch ) )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  pm2.61da3ne  2526  rmob  3079  disjxiun  4020  f1imass  5788  soisoi  5825  riota5f  6329  tfrlem9a  6402  oeeui  6600  oaabs2  6643  omabs  6645  omxpenlem  6963  fopwdom  6970  frfi  7102  marypha1lem  7186  ordiso2  7230  oismo  7255  wemaplem3  7263  cantnf  7395  isinffi  7625  dfac12lem2  7770  dfac12lem3  7771  infxp  7841  infmap2  7844  infpssrlem5  7933  fin23lem11  7943  fin23lem24  7948  fin23lem26  7951  isf32lem2  7980  isf32lem4  7982  fin1a2lem13  8038  fin1a2s  8040  ttukeylem5  8140  fpwwe2lem12  8263  fpwwe2lem13  8264  wunex2  8360  tskord  8402  prlem934  8657  addid1  8992  cnegex  8993  negeu  9042  add20  9286  divdivdiv  9461  ltmul12a  9612  lediv12a  9649  cru  9738  uzwo3  10311  xleadd1a  10573  xlemul1a  10608  ixxun  10672  ixxss12  10676  mulexpz  11142  leexp1a  11160  expmulnbnd  11233  abs3lem  11822  rexanre  11830  cau3lem  11838  lo1bdd2  11998  o1lo1  12011  rlimclim1  12019  rlimclim  12020  lo1resb  12038  o1resb  12040  rlimcn2  12064  o1of2  12086  o1rlimmul  12092  lo1add  12100  lo1mul  12101  isercolllem1  12138  climcau  12144  summolem2  12189  summo  12190  o1fsum  12271  qredeu  12786  isprm5  12791  pclem  12891  pcqmul  12906  pcexp  12912  pcneg  12926  pcprmpw2  12934  pcadd  12937  prmpwdvds  12951  4sqlem13  13004  vdwlem2  13029  vdwlem7  13034  vdwlem11  13038  vdwlem12  13039  ramval  13055  ramz2  13071  ramcl  13076  imasval  13414  imasdsval  13418  mreexexd  13550  issubc3  13723  idfucl  13755  funcres2c  13775  fucpropd  13851  xpcval  13951  prfval  13973  evlfcl  13996  curf12  14001  curf1cl  14002  curf2  14003  curfcl  14006  curfuncf  14012  curf2ndf  14021  hof2val  14030  hofcl  14033  hofpropd  14041  yonedalem4a  14049  yonedainv  14055  poslubmo  14250  isipodrs  14264  acsmapd  14281  acsinfd  14283  mndpropd  14398  mhmeql  14441  frmdup3  14488  issubg4  14638  ssnmz  14659  sylow2blem3  14933  lsmdisj2  14991  pj1eu  15005  efgredlem  15056  frgpuplem  15081  frgpnabl  15163  dmdprdsplitlem  15272  pgpfac1lem3  15312  pgpfaclem3  15318  rngpropd  15372  dvdsrtr  15434  islmhm2  15795  lmhmpropd  15826  assapropd  16067  coe1tmmul2  16352  prmirredlem  16446  lsmcss  16592  toponmre  16830  restbas  16889  iscncl  16998  cnpdis  17021  lmcnp  17032  dishaus  17110  cmpcovf  17118  hauscmplem  17133  dfcon2  17145  clscon  17156  2ndcctbss  17181  1stccnp  17188  islly2  17210  llyidm  17214  cldllycmp  17221  kgentopon  17233  1stckgenlem  17248  ptpjpre1  17266  ptbasfi  17276  txcls  17299  ptpjopn  17306  xkoccn  17313  txcnp  17314  txcmpb  17338  xkoptsub  17348  xkoco2cn  17352  xkoinjcn  17381  qtopcn  17405  qtoprest  17408  regr1lem  17430  regr1lem2  17431  kqreglem1  17432  qtophmeo  17508  fgabs  17574  hauspwpwf1  17682  flimfnfcls  17723  fclscmp  17725  cnpfcf  17736  ptcmplem4  17749  ptcmplem5  17750  tmdgsum2  17779  tsmsval2  17812  ismet2  17898  blin  17970  metss2lem  18057  methaus  18066  met1stc  18067  met2ndci  18068  metcnp  18087  metcnpi3  18092  nlmvscn  18198  nrginvrcn  18202  nghmcn  18254  xrsxmet  18315  reconnlem1  18331  reconn  18333  xrge0tsms  18339  xmetdcn2  18342  metdscn  18360  addcnlem  18368  mulc1cncf  18409  cncfco  18411  cnheiborlem  18452  cnheibor  18453  nmoleub2lem2  18597  ipcn  18673  iscfil3  18699  cfilfcls  18700  iscmet3  18719  caubl  18733  bcthlem5  18750  minveclem3b  18792  minveclem7  18799  pmltpc  18810  ovolshftlem1  18868  ovolscalem1  18872  ioombl1  18919  uniioombllem6  18943  dyadss  18949  dyaddisjlem  18950  dyadmax  18953  opnmbllem  18956  itg1addlem2  19052  itg2seq  19097  bddmulibl  19193  limcfval  19222  ellimc3  19229  limciun  19244  dveflem  19326  rolle  19337  dvlip2  19342  c1liplem1  19343  dvgt0lem1  19349  dvgt0  19351  dvlt0  19352  dvne0  19358  dvcnvre  19366  dvfsumrlimge0  19377  ftc1lem6  19388  itgsubst  19396  evlslem1  19399  mdegmullem  19464  ply1domn  19509  fta1g  19553  fta1b  19555  dgrlem  19611  coeid  19620  plydivalg  19679  aannenlem1  19708  aalioulem6  19717  ulmcn  19776  abelthlem8  19815  efif1olem4  19907  chordthm  20134  xrlimcnp  20263  isppw2  20353  fsumvma2  20453  perfectlem2  20469  lgsdilem  20561  lgsquad2lem2  20598  lgsquad3  20600  2sqlem5  20607  2sqlem9  20612  rpvmasumlem  20636  dchrisum0flb  20659  pntpbnd  20737  pntibndlem3  20741  pntlem3  20758  pntleml  20760  vacn  21267  ubthlem1  21449  ubthlem3  21451  minvecolem7  21462  chocunii  21880  pjhthmo  21881  pjhthlem2  21971  nmopub2tALT  22489  nmfnleub2  22506  kbass5  22700  mdslmd1lem1  22905  mdslmd1lem2  22906  mdsymlem5  22987  ballotlemsf1o  23072  xrofsup  23255  xrge0tsmsd  23382  esumpcvgval  23446  imambfm  23567  pconcon  23762  conpcon  23766  cvmliftmo  23815  cvmlift2lem10  23843  cvmlift2lem12  23845  cvmlift3lem7  23856  eupath2  23904  dedekind  24082  axsegcon  24555  axpasch  24569  axeuclidlem  24590  ifscgr  24667  cgrxfr  24678  btwnconn1lem13  24722  ellines  24775  muldisc  25481  limptlimpr2lem1  25574  limptlimpr2lem2  25575  trnij  25615  icccon2  25700  imonclem  25813  idmon  25817  locfincmp  26304  sstotbnd  26499  cntotbnd  26520  ismtyima  26527  heibor1lem  26533  heiborlem10  26544  bfp  26548  rrncmslem  26556  isnacs3  26785  nacsfix  26787  mzpsubst  26826  eldioph2lem2  26840  eldioph2  26841  eldioph2b  26842  diophin  26852  diophun  26853  rencldnfilem  26903  irrapxlem3  26909  irrapxlem5  26911  pell1234qrreccl  26939  pell1234qrmulcl  26940  pell1qrge1  26955  pell1qrgaplem  26958  monotuz  27026  monotoddzzfi  27027  rpexpmord  27033  acongtr  27065  acongrep  27067  jm2.26a  27093  jm2.26lem3  27094  jm2.26  27095  jm2.27b  27099  jm2.27  27101  wepwsolem  27138  fnwe2lem2  27148  dsmmlss  27210  uvcf1  27241  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  fnchoice  27700  rfcnnnub  27707  stoweidlem14  27763  stoweidlem27  27776  stoweidlem31  27780  stoweidlem34  27783  stoweidlem49  27798  stoweidlem56  27805  islshpsm  29170  lsatcmp  29193  islshpat  29207  lfl0f  29259  iscvlat2N  29514  ishlat3N  29544  3dim1  29656  islvol5  29768  lvoli2  29770  lncvrelatN  29970  lncmp  29972  paddasslem10  30018  pclfinclN  30139  pexmidlem8N  30166  idltrn  30339  cdleme42keg  30675  cdleme42mgN  30677  cdlemf2  30751  cdlemg2cex  30780  trlcoat  30912  tendoex  31164  erngdvlem4  31180  erngdvlem4-rN  31188  dialss  31236  dibglbN  31356  diblss  31360  dihlsscpre  31424  dihglblem2aN  31483  dihglblem4  31487  dihglblem5  31488  dih1dimatlem  31519  dihglblem6  31530  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