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

Theorem simplll 766
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 458 . 2  |-  ( (
ph  /\  ps )  ->  ph )
21ad2antrr 730 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  simp-4l  774  f1imass  6172  oeeui  7303  oaabs2  7346  boxcutc  7565  omxpenlem  7671  cantnfle  8173  acndom2  8481  infpwfien  8489  sornom  8703  isf32lem2  8780  isf32lem4  8782  fin1a2lem11  8836  ttukeylem5  8939  pwfseq  9085  gchina  9120  inttsk  9195  inar1  9196  prlem936  9468  mulcmpblnr  9491  00id  9804  mul02lem1  9805  addid1  9809  cnegex  9810  negeu  9861  add20  10122  ltmul12a  10457  lediv12a  10495  fiminre  10551  cru  10597  qextltlem  11491  xmullem  11546  xlemul1a  11570  ixxss12  11651  ioodisj  11756  elfz0fzfz0  11889  fsuppmapnn0fz  12201  seqf1o  12247  mulexpz  12305  leexp1a  12324  seqcoll  12617  swrdswrdlem  12796  abs3lem  13380  cau3lem  13396  climcau  13712  sumeq2ii  13737  summolem2  13760  climcndslem1  13885  climcndslem2  13886  geomulcvg  13910  mertenslem1  13918  mertenslem2  13919  mertens  13920  prodeq2ii  13945  prodmolem2  13967  bitsfzo  14387  sadadd2lem2  14402  dvdsmulgcd  14500  qredeu  14642  pc2dvds  14806  pcz  14808  ramcl  14965  firest  15309  mreexexlemd  15528  isacs2  15537  iscatd2  15565  ipodrsima  16389  mrelatlub  16410  mndpropd  16540  mhmeql  16589  isgrpinv  16694  mulgnn0dir  16759  mhmid  16785  mhmmnd  16786  issubg4  16814  gasubg  16934  symgextf  17036  pmtr3ncom  17094  gexdvds  17213  oddvdssubg  17471  cyggeninv  17496  cyggenod  17497  issrg  17719  dvdsrmul1  17859  unitgrp  17873  cntzsubr  18018  islmhm2  18239  lmhmeql  18256  lbspropd  18300  lssacsex  18345  issubassa2  18547  mplbas2  18672  psgndiflemA  19146  isphl  19172  ocvocv  19211  lindfmm  19362  scmatmats  19513  smatvscl  19526  mdetdiag  19601  m2cpmfo  19757  pmatcollpw3fi1lem1  19787  pm2mpf1  19800  pm2mpghm  19817  fvmptnn04if  19850  chfacfscmulfsupp  19860  chfacfpmmulfsupp  19864  neissex  20120  neiptoptop  20124  neiptopnei  20125  restbas  20151  tgrest  20152  restopnb  20168  cnpco  20260  isnrm3  20352  isreg2  20370  iuncon  20420  1stcrest  20445  2ndcctbss  20447  2ndcomap  20450  2ndcsep  20451  dislly  20489  kgencn2  20549  ptbasfi  20573  txhaus  20639  txkgen  20644  txcon  20681  qtopcn  20706  regr1lem2  20732  kqnrmlem1  20735  kqnrmlem2  20736  trfbas2  20835  trfil2  20879  flimcf  20974  hauspwpwf1  20979  fclscf  21017  flimfnfcls  21020  cnextcn  21059  ustexsym  21207  ustex2sym  21208  ustex3sym  21209  ustuqtop4  21236  utop3cls  21243  utopreg  21244  ucnima  21273  ucncn  21277  fmucnd  21284  metequiv2  21502  prdsxmslem2  21521  metcnpi3  21538  metustto  21545  metustid  21546  metustexhalf  21548  ngptgp  21621  xrsblre  21806  icccmp  21820  reconnlem1  21821  reconn  21823  opnreen  21826  metdsf  21842  metdscn  21850  metdsfOLD  21857  metdscnOLD  21865  fsumcn  21879  elcncf2  21899  cncfmet  21917  pcoass  22032  lmcau  22259  rrxdstprj1  22340  pmltpc  22378  ivthlem2  22380  ivthlem3  22381  ovollb2  22419  volsup  22486  ioombl1  22492  ioorf  22502  ioorfOLD  22507  dyadss  22529  dyaddisjlem  22530  dyadmax  22533  volcn  22541  cncombf  22591  mbflimsup  22600  mbflimsupOLD  22601  itg2const2  22676  iblss2  22740  cpnord  22866  dvmptfsum  22904  fta1g  23095  plydivex  23227  fta1  23238  aannenlem1  23261  ulmdvlem3  23334  abelthlem8  23371  pilem3  23386  pilem3OLD  23387  advlogexp  23577  cxpmul2z  23613  atantayl2  23841  jensen  23891  isppw2  24019  lgsqr  24251  lgsdchrval  24252  lgsquad3  24266  2sqb  24283  dchrisumlem3  24306  rpvmasum2  24327  mulog2sumlem2  24350  pntrsumbnd2  24382  f1otrg  24878  f1otrge  24879  axsegcon  24934  axeuclidlem  24969  axcontlem9  24979  eengtrkg  24992  nbgraf1olem5  25149  cusgrasize2inds  25181  0wlkon  25253  0trlon  25254  0pthon  25285  3v3e3cycl2  25368  wlkiswwlk1  25394  usg2wotspth  25588  vdiscusgra  25625  iseupa  25669  vdn1frgrav2  25729  vdgn1frgrav2  25730  frgrancvvdeqlem9  25745  frgrawopreg  25753  frghash2spot  25767  numclwlk1lem2foa  25795  numclwlk1lem2fo  25799  frgrareggt1  25820  vacn  26306  smcnlem  26309  0lno  26407  chocunii  26930  occl  26933  5oalem1  27283  3oalem2  27292  unoplin  27549  hmoplin  27571  lnconi  27662  kbass5  27749  mdslmd1lem1  27954  mdslmd1lem2  27955  mdsymlem2  28033  cdj1i  28062  disjabrex  28172  disjabrexf  28173  acunirnmpt  28242  fgreu  28255  xrge0infss  28325  xrge0infssOLD  28326  xrofsup  28338  xrge0addgt0  28442  submomnd  28461  submarchi  28491  archiabllem1  28498  archiabllem2a  28499  isarchiofld  28569  locfinreflem  28656  rge0scvg  28744  lmxrge0  28747  lmdvg  28748  qqhval2  28775  esumrnmpt2  28878  esumfsup  28880  esumpcvgval  28888  esumcvg  28896  esumgect  28900  esumiun  28904  sigaclfu2  28932  sigainb  28947  insiga  28948  fiunelros  28985  measinblem  29031  measinb  29032  measdivcstOLD  29035  measdivcst  29036  omssubadd  29117  omssubaddOLD  29121  oddpwdc  29176  dstrvprob  29293  sgnmul  29402  sgnsub  29404  signsply0  29429  signstfvneq0  29450  bnj1408  29834  ptpcon  29945  sconpi1  29951  rescon  29958  cvmliftmolem2  29994  cvmlift2lem12  30026  poseq  30479  ifscgr  30797  cgrxfr  30808  outsideofeu  30884  linethru  30906  neibastop1  31001  fin2so  31840  poimirlem28  31876  poimirlem31  31879  mblfinlem2  31886  mblfinlem3  31887  itg2addnclem  31901  ftc1anclem7  31931  ftc1anclem8  31932  ftc1anc  31933  ssbnd  32028  totbndbnd  32029  prtlem10  32349  lssats  32491  lkrlss  32574  lshpset2N  32598  2dim  32948  islvol5  33057  paddasslem11  33308  pexmidlem8N  33455  ltrnid  33613  idltrn  33628  trlator0  33650  trlnidatb  33656  cdlemf2  34042  cdlemg2cex  34071  tendodi1  34264  tendodi2  34265  diblss  34651  dihopelvalcpre  34729  dih1dimatlem  34810  dihglblem6  34821  mzpsubst  35503  mzpcompact2lem  35506  eldioph2  35517  eldioph2b  35518  diophren  35569  pell14qrexpcl  35627  elpell1qr2  35632  monotoddzzfi  35704  acongtr  35742  acongrep  35744  jm2.19lem4  35761  jm2.26a  35769  jm2.26lem3  35770  jm2.26  35771  isnumbasgrplem2  35877  mendassa  35974  prmunb2  36511  4an4132  36707  adant423  37222  fiiuncl  37263  supxrgelem  37384  mullimc  37483  mullimcf  37490  neglimc  37515  icccncfext  37552  cncfiooicclem1  37558  fprodcncf  37566  dvnprodlem3  37610  iblcncfioo  37642  itgspltprt  37643  stoweidlem7  37654  stoweidlem28  37675  stoweidlem34  37682  stoweidlem48  37696  stoweidlem52  37700  wallispilem3  37716  fourierdlem12  37768  fourierdlem38  37795  fourierdlem39  37796  fourierdlem42  37799  fourierdlem42OLD  37800  fourierdlem46  37803  fourierdlem48  37805  fourierdlem49  37806  fourierdlem50  37807  fourierdlem51  37808  fourierdlem65  37822  fourierdlem73  37830  fourierdlem76  37833  fourierdlem87  37844  fourierdlem103  37860  fourierdlem104  37861  sge0f1o  37979  sge0le  38004  ismeannd  38035  nnsum4primeseven  38515  nnsum4primesevenALTV  38516  bgoldbtbndlem2  38521  bgoldbtbndlem3  38522  bgoldbtbnd  38524  ralxfrd2  38617  mgmhmeql  38865
  Copyright terms: Public domain W3C validator