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

Theorem simplll 757
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 457 . 2  |-  ( (
ph  /\  ps )  ->  ph )
21ad2antrr 725 1  |-  ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  simp-4l  765  f1imass  6160  tfrlem1  7045  oeeui  7251  oaabs2  7294  boxcutc  7512  omxpenlem  7618  cantnfle  8090  cantnfleOLD  8120  acndom2  8435  infpwfien  8443  sornom  8657  isf32lem2  8734  isf32lem4  8736  fin1a2lem11  8790  ttukeylem5  8893  pwfseq  9042  gchina  9077  inttsk  9152  inar1  9153  prlem936  9425  mulcmpblnr  9448  00id  9754  mul02lem1  9755  addid1  9759  cnegex  9760  negeu  9810  add20  10064  ltmul12a  10398  lediv12a  10438  cru  10528  qextltlem  11401  xmullem  11456  xlemul1a  11480  ixxss12  11549  ioodisj  11650  elfz0fzfz0  11777  fsuppmapnn0fz  12070  seqf1o  12116  mulexpz  12174  leexp1a  12192  seqcoll  12478  swrdswrdlem  12647  abs3lem  13134  cau3lem  13150  climcau  13456  sumeq2ii  13478  summolem2  13501  climcndslem1  13624  climcndslem2  13625  geomulcvg  13648  mertenslem1  13656  mertenslem2  13657  mertens  13658  bitsfzo  13944  sadadd2lem2  13959  dvdsmulgcd  14051  qredeu  14107  pc2dvds  14261  pcz  14263  ramcl  14406  firest  14688  mreexexlemd  14899  isacs2  14908  iscatd2  14936  ipodrsima  15652  mrelatlub  15673  mndpropd  15764  mhmeql  15814  isgrpinv  15910  mulgnn0dir  15975  issubg4  16025  gasubg  16145  symgextf  16247  pmtr3ncom  16306  gexdvds  16410  oddvdssubg  16664  cyggeninv  16689  cyggenod  16690  issrg  16961  dvdsrmul1  17103  unitgrp  17117  cntzsubr  17261  islmhm2  17484  lmhmeql  17501  lbspropd  17545  lssacsex  17590  issubassa2  17793  mplbas2  17933  mplbas2OLD  17934  psgndiflemA  18432  isphl  18458  ocvocv  18497  lindfmm  18657  scmatmats  18808  smatvscl  18821  mdetdiag  18896  m2cpmfo  19052  pmatcollpw3fi1lem1  19082  pm2mpf1  19095  pm2mpghm  19112  fvmptnn04if  19145  chfacfscmulfsupp  19155  chfacfpmmulfsupp  19159  neissex  19422  neiptoptop  19426  neiptopnei  19427  restbas  19453  tgrest  19454  restopnb  19470  cnpco  19562  isnrm3  19654  isreg2  19672  iuncon  19723  1stcrest  19748  2ndcctbss  19750  2ndcomap  19753  2ndcsep  19754  dislly  19792  kgencn2  19821  ptbasfi  19845  txhaus  19911  txkgen  19916  txcon  19953  qtopcn  19978  regr1lem2  20004  kqnrmlem1  20007  kqnrmlem2  20008  trfbas2  20107  trfil2  20151  flimcf  20246  hauspwpwf1  20251  fclscf  20289  flimfnfcls  20292  cnextcn  20330  ustexsym  20481  ustex2sym  20482  ustex3sym  20483  ustuqtop4  20510  utop3cls  20517  utopreg  20518  ucnima  20547  ucncn  20551  fmucnd  20558  metequiv2  20776  prdsxmslem2  20795  metcnpi3  20812  metusttoOLD  20823  metustto  20824  metustidOLD  20825  metustid  20826  metustexhalfOLD  20829  metustexhalf  20830  ngptgp  20913  xrsblre  21079  icccmp  21093  reconnlem1  21094  reconn  21096  opnreen  21099  metdsf  21115  metdscn  21123  fsumcn  21137  elcncf2  21157  cncfmet  21175  pcoass  21287  lmcau  21514  rrxdstprj1  21599  pmltpc  21625  ivthlem2  21627  ivthlem3  21628  ovollb2  21663  volsup  21729  ioombl1  21735  ioorf  21745  dyadss  21766  dyaddisjlem  21767  dyadmax  21770  volcn  21778  cncombf  21828  mbflimsup  21836  itg2const2  21911  iblss2  21975  cpnord  22101  dvmptfsum  22139  fta1g  22331  plydivex  22455  fta1  22466  aannenlem1  22486  ulmdvlem3  22559  abelthlem8  22596  pilem3  22610  advlogexp  22792  cxpmul2z  22828  atantayl2  23025  jensen  23074  isppw2  23145  lgsqr  23377  lgsdchrval  23378  lgsquad3  23392  2sqb  23409  dchrisumlem3  23432  rpvmasum2  23453  mulog2sumlem2  23476  pntrsumbnd2  23508  f1otrg  23878  f1otrge  23879  axsegcon  23934  axeuclidlem  23969  axcontlem9  23979  eengtrkg  23992  nbgraf1olem5  24149  cusgrasize2inds  24181  0wlkon  24253  0trlon  24254  0pthon  24285  3v3e3cycl2  24368  wlkiswwlk1  24394  usg2wotspth  24588  vdiscusgra  24625  iseupa  24669  vdn1frgrav2  24730  vdgn1frgrav2  24731  frgrancvvdeqlem9  24746  frgrawopreg  24754  frghash2spot  24768  numclwlk1lem2foa  24796  numclwlk1lem2fo  24800  frgrareggt1  24821  vacn  25308  smcnlem  25311  0lno  25409  chocunii  25923  occl  25926  5oalem1  26276  3oalem2  26285  unoplin  26543  hmoplin  26565  lnconi  26656  kbass5  26743  mdslmd1lem1  26948  mdslmd1lem2  26949  mdsymlem2  27027  cdj1i  27056  disjabrex  27144  disjabrexf  27145  fgreu  27213  xrge0infss  27276  xrofsup  27278  xrge0addgt0  27371  submomnd  27390  submarchi  27420  archiabllem1  27427  archiabllem2a  27428  isarchiofld  27498  rge0scvg  27595  lmxrge0  27598  lmdvg  27599  qqhval2  27627  esumfsup  27744  esumpcvgval  27752  esumcvg  27760  sigaclfu2  27789  sigainb  27804  insiga  27805  measinblem  27859  measinb  27860  measdivcstOLD  27863  measdivcst  27864  oddpwdc  27961  dstrvprob  28078  sgnmul  28149  sgnsub  28151  signsply0  28176  signstfvneq0  28197  ptpcon  28346  sconpi1  28352  rescon  28359  cvmliftmolem2  28395  cvmlift2lem12  28427  prodeq2ii  28650  prodmolem2  28672  poseq  28938  ifscgr  29299  cgrxfr  29310  outsideofeu  29386  linethru  29408  fin2so  29645  mblfinlem2  29657  mblfinlem3  29658  itg2addnclem  29671  ftc1anclem7  29701  ftc1anclem8  29702  ftc1anc  29703  neibastop1  29808  ssbnd  29915  totbndbnd  29916  prtlem10  30238  mzpsubst  30313  mzpcompact2lem  30316  eldioph2  30327  eldioph2b  30328  diophren  30379  pell14qrexpcl  30435  elpell1qr2  30440  monotoddzzfi  30510  acongtr  30548  acongrep  30550  jm2.19lem4  30566  jm2.26a  30574  jm2.26lem3  30575  jm2.26  30576  isnumbasgrplem2  30685  mendassa  30776  prmunb2  30822  adant423  31035  mullimc  31186  mullimcf  31193  neglimc  31217  icccncfext  31254  cncfiooicclem1  31260  dvbdfbdioolem2  31287  iblcncfioo  31324  itgspltprt  31325  stoweidlem7  31335  stoweidlem28  31356  stoweidlem34  31362  stoweidlem48  31376  stoweidlem49  31377  stoweidlem52  31380  stoweidlem57  31385  wallispilem3  31395  fourierdlem12  31447  fourierdlem38  31473  fourierdlem39  31474  fourierdlem42  31477  fourierdlem46  31481  fourierdlem48  31483  fourierdlem49  31484  fourierdlem50  31485  fourierdlem51  31486  fourierdlem65  31500  fourierdlem73  31508  fourierdlem76  31511  fourierdlem87  31522  fourierdlem103  31538  fourierdlem104  31539  ralxfrd2  31798  4animp1  32363  4an4132  32365  bnj1408  33189  lssats  33827  lkrlss  33910  lshpset2N  33934  2dim  34284  islvol5  34393  paddasslem11  34644  pexmidlem8N  34791  ltrnid  34949  idltrn  34964  trlator0  34985  trlnidatb  34991  cdlemf2  35376  cdlemg2cex  35405  tendodi1  35598  tendodi2  35599  diblss  35985  dihopelvalcpre  36063  dih1dimatlem  36144  dihglblem6  36155
  Copyright terms: Public domain W3C validator