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

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

Proof of Theorem simplll
StepHypRef Expression
1 simpl 443 . 2  |-  ( (
ph  /\  ps )  ->  ph )
21ad2antrr 706 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  simp-4l  742  f1imass  5788  oeeui  6600  oaabs2  6643  boxcutc  6859  omxpenlem  6963  cantnfle  7372  acndom2  7681  infpwfien  7689  sornom  7903  isf32lem2  7980  isf32lem4  7982  fin1a2lem11  8036  ttukeylem5  8140  pwfseq  8286  gchina  8321  inttsk  8396  inar1  8397  prlem936  8671  00id  8987  mul02lem1  8988  addid1  8992  cnegex  8993  negeu  9042  add20  9286  ltmul12a  9612  lediv12a  9649  cru  9738  qextltlem  10529  xmullem  10584  xlemul1a  10608  ixxss12  10676  ioodisj  10765  seqf1o  11087  mulexpz  11142  leexp1a  11160  seqcoll  11401  abs3lem  11822  cau3lem  11838  climcau  12144  sumeq2ii  12166  summolem2  12189  climcndslem1  12308  climcndslem2  12309  geomulcvg  12332  mertenslem1  12340  mertenslem2  12341  mertens  12342  bitsfzo  12626  sadadd2lem2  12641  dvdsmulgcd  12733  qredeu  12786  pc2dvds  12931  pcz  12933  ramcl  13076  firest  13337  mreexexlemd  13546  isacs2  13555  iscatd2  13583  ipodrsima  14268  mrelatlub  14289  mndpropd  14398  mhmeql  14441  isgrpinv  14532  mulgnn0dir  14590  issubg4  14638  gasubg  14756  gexdvds  14895  oddvdssubg  15147  cyggeninv  15170  cyggenod  15171  dvdsrmul1  15435  unitgrp  15449  cntzsubr  15577  islmhm2  15795  lmhmeql  15812  lbspropd  15852  lssacsex  15897  issubassa2  16084  mplbas2  16212  isphl  16532  ocvocv  16571  neissex  16864  restbas  16889  tgrest  16890  restopnb  16906  cnpco  16996  isnrm3  17087  isreg2  17105  iuncon  17154  1stcrest  17179  2ndcctbss  17181  2ndcomap  17184  2ndcsep  17185  dislly  17223  kgencn2  17252  ptbasfi  17276  txhaus  17341  txkgen  17346  txcon  17383  qtopcn  17405  regr1lem2  17431  kqreglem1  17432  kqnrmlem1  17434  kqnrmlem2  17435  trfbas2  17538  trfil2  17582  flimcf  17677  hauspwpwf1  17682  fclscf  17720  flimfnfcls  17723  metequiv2  18056  prdsxmslem2  18075  metcnpi3  18092  ngptgp  18152  xrsblre  18317  icccmp  18330  reconnlem1  18331  reconn  18333  opnreen  18336  xrge0tsms  18339  xmetdcn2  18342  metdsf  18352  metdscn  18360  fsumcn  18374  elcncf2  18394  cncfmet  18412  pcoass  18522  iscfil2  18692  iscfil3  18699  lmcau  18738  pmltpc  18810  ivthlem2  18812  ivthlem3  18813  ovollb2  18848  volsup  18913  ioombl1  18919  ioorf  18928  uniioombl  18944  dyadss  18949  dyaddisjlem  18950  dyadmax  18953  volcn  18961  cncombf  19013  mbflimsup  19021  itg2const2  19096  iblss2  19160  cpnord  19284  dvmptfsum  19322  fta1g  19553  plydivex  19677  fta1  19688  aannenlem1  19708  ulmdvlem3  19779  abelthlem8  19815  pilem3  19829  advlogexp  20002  cxpmul2z  20038  atantayl2  20234  jensen  20283  isppw2  20353  dchrptlem1  20503  lgsdchrval  20586  lgsquad3  20600  2sqb  20617  dchrisumlem3  20640  rpvmasum2  20661  mulog2sumlem2  20684  pntrsumbnd2  20716  pntpbnd  20737  vacn  21267  smcnlem  21270  0lno  21368  chocunii  21880  occl  21883  5oalem1  22233  3oalem2  22242  unoplin  22500  hmoplin  22522  lnconi  22613  kbass5  22700  mdslmd1lem1  22905  mdslmd1lem2  22906  mdsymlem2  22984  cdj1i  23013  xrofsup  23255  xrge0addgt0  23331  disjabrex  23359  disjabrexf  23360  rge0scvg  23373  lmxrge0  23375  lmdvg  23376  xrge0tsmsd  23382  esumpcvgval  23446  esumcvg  23454  sigaclfu2  23482  sigainb  23497  insiga  23498  measinblem  23547  measinb  23548  measdivcstOLD  23551  measdivcst  23552  dstrvprob  23672  ptpcon  23764  sconpi1  23770  rescon  23777  cvmliftmolem2  23813  cvmlift2lem12  23845  iseupa  23881  poseq  24253  axsegcon  24555  axeuclidlem  24590  axcontlem9  24600  ifscgr  24667  cgrxfr  24678  outsideofeu  24754  linethru  24776  muldisc  25481  glmrngo  25482  limptlimpr2lem2  25575  tcnvec  25690  neibastop1  26308  ssbnd  26512  totbndbnd  26513  prtlem10  26733  mzpsubst  26826  mzpcompact2lem  26829  eldioph2  26841  eldioph2b  26842  diophren  26896  pell14qrexpcl  26952  elpell1qr2  26957  monotoddzzfi  27027  acongtr  27065  acongrep  27067  jm2.19lem4  27085  jm2.26a  27093  jm2.26lem3  27094  jm2.26  27095  isnumbasgrplem2  27269  lindfmm  27297  mendassa  27502  fnchoice  27700  stoweidlem7  27756  stoweidlem28  27777  stoweidlem34  27783  stoweidlem35  27784  stoweidlem48  27797  stoweidlem49  27798  stoweidlem52  27801  stoweidlem57  27806  stoweidlem60  27809  wallispilem3  27816  bnj1408  29066  lssats  29202  lkrlss  29285  lshpset2N  29309  2dim  29659  islvol5  29768  paddasslem11  30019  pexmidlem8N  30166  ltrnid  30324  idltrn  30339  trlator0  30360  trlnidatb  30366  cdlemf2  30751  cdlemg2cex  30780  tendodi1  30973  tendodi2  30974  diblss  31360  dihopelvalcpre  31438  dih1dimatlem  31519  dihglblem6  31530
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