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  5830  oeeui  6642  oaabs2  6685  boxcutc  6902  omxpenlem  7006  cantnfle  7417  acndom2  7726  infpwfien  7734  sornom  7948  isf32lem2  8025  isf32lem4  8027  fin1a2lem11  8081  ttukeylem5  8185  pwfseq  8331  gchina  8366  inttsk  8441  inar1  8442  prlem936  8716  00id  9032  mul02lem1  9033  addid1  9037  cnegex  9038  negeu  9087  add20  9331  ltmul12a  9657  lediv12a  9694  cru  9783  qextltlem  10576  xmullem  10631  xlemul1a  10655  ixxss12  10723  ioodisj  10812  seqf1o  11134  mulexpz  11189  leexp1a  11207  seqcoll  11448  abs3lem  11869  cau3lem  11885  climcau  12191  sumeq2ii  12213  summolem2  12236  climcndslem1  12355  climcndslem2  12356  geomulcvg  12379  mertenslem1  12387  mertenslem2  12388  mertens  12389  bitsfzo  12673  sadadd2lem2  12688  dvdsmulgcd  12780  qredeu  12833  pc2dvds  12978  pcz  12980  ramcl  13123  firest  13386  mreexexlemd  13595  isacs2  13604  iscatd2  13632  ipodrsima  14317  mrelatlub  14338  mndpropd  14447  mhmeql  14490  isgrpinv  14581  mulgnn0dir  14639  issubg4  14687  gasubg  14805  gexdvds  14944  oddvdssubg  15196  cyggeninv  15219  cyggenod  15220  dvdsrmul1  15484  unitgrp  15498  cntzsubr  15626  islmhm2  15844  lmhmeql  15861  lbspropd  15901  lssacsex  15946  issubassa2  16133  mplbas2  16261  isphl  16588  ocvocv  16627  neissex  16920  restbas  16945  tgrest  16946  restopnb  16962  cnpco  17052  isnrm3  17143  isreg2  17161  iuncon  17210  1stcrest  17235  2ndcctbss  17237  2ndcomap  17240  2ndcsep  17241  dislly  17279  kgencn2  17308  ptbasfi  17332  txhaus  17397  txkgen  17402  txcon  17439  qtopcn  17461  regr1lem2  17487  kqreglem1  17488  kqnrmlem1  17490  kqnrmlem2  17491  trfbas2  17590  trfil2  17634  flimcf  17729  hauspwpwf1  17734  fclscf  17772  flimfnfcls  17775  metequiv2  18108  prdsxmslem2  18127  metcnpi3  18144  ngptgp  18204  xrsblre  18369  icccmp  18382  reconnlem1  18383  reconn  18385  opnreen  18388  xrge0tsms  18391  xmetdcn2  18394  metdsf  18404  metdscn  18412  fsumcn  18426  elcncf2  18446  cncfmet  18464  pcoass  18575  iscfil2  18745  iscfil3  18752  lmcau  18791  pmltpc  18863  ivthlem2  18865  ivthlem3  18866  ovollb2  18901  volsup  18966  ioombl1  18972  ioorf  18981  uniioombl  18997  dyadss  19002  dyaddisjlem  19003  dyadmax  19006  volcn  19014  cncombf  19066  mbflimsup  19074  itg2const2  19149  iblss2  19213  cpnord  19337  dvmptfsum  19375  fta1g  19606  plydivex  19730  fta1  19741  aannenlem1  19761  ulmdvlem3  19832  abelthlem8  19868  pilem3  19882  advlogexp  20055  cxpmul2z  20091  atantayl2  20287  jensen  20336  isppw2  20406  dchrptlem1  20556  lgsdchrval  20639  lgsquad3  20653  2sqb  20670  dchrisumlem3  20693  rpvmasum2  20714  mulog2sumlem2  20737  pntrsumbnd2  20769  pntpbnd  20790  vacn  21322  smcnlem  21325  0lno  21423  chocunii  21935  occl  21938  5oalem1  22288  3oalem2  22297  unoplin  22555  hmoplin  22577  lnconi  22668  kbass5  22755  mdslmd1lem1  22960  mdslmd1lem2  22961  mdsymlem2  23039  cdj1i  23068  disjabrex  23167  disjabrexf  23168  xrofsup  23272  xrge0addgt0  23352  xrge0tsmsd  23360  rge0scvg  23404  lmxrge0  23406  lmdvg  23407  ucnima  23474  fmucnd  23484  metustto  23495  metustid  23496  metustexhalf  23498  qqhval2  23561  esumfsup  23636  esumpcvgval  23644  esumcvg  23652  sigaclfu2  23680  sigainb  23695  insiga  23696  measinblem  23748  measinb  23749  measdivcstOLD  23752  measdivcst  23753  dstrvprob  23903  ptpcon  24048  sconpi1  24054  rescon  24061  cvmliftmolem2  24097  cvmlift2lem12  24129  iseupa  24165  prodeq2ii  24416  prodmolem2  24438  poseq  24638  axsegcon  24941  axeuclidlem  24976  axcontlem9  24986  ifscgr  25053  cgrxfr  25064  outsideofeu  25140  linethru  25162  itg2addnclem  25317  neibastop1  25457  ssbnd  25660  totbndbnd  25661  prtlem10  25881  mzpsubst  25974  mzpcompact2lem  25977  eldioph2  25989  eldioph2b  25990  diophren  26044  pell14qrexpcl  26100  elpell1qr2  26105  monotoddzzfi  26175  acongtr  26213  acongrep  26215  jm2.19lem4  26233  jm2.26a  26241  jm2.26lem3  26242  jm2.26  26243  isnumbasgrplem2  26417  lindfmm  26445  mendassa  26650  fnchoice  26848  stoweidlem7  26904  stoweidlem28  26925  stoweidlem34  26931  stoweidlem35  26932  stoweidlem48  26945  stoweidlem49  26946  stoweidlem52  26949  stoweidlem57  26954  stoweidlem60  26957  wallispilem3  26964  nbgraf1olem5  27392  0wlkon  27459  0trlon  27460  0pthon  27481  3v3e3cycl2  27548  vdn1frgrav2  27618  vdgn1frgrav2  27619  frgrancvvdeqlem9  27633  bnj1408  28577  lssats  29020  lkrlss  29103  lshpset2N  29127  2dim  29477  islvol5  29586  paddasslem11  29837  pexmidlem8N  29984  ltrnid  30142  idltrn  30157  trlator0  30178  trlnidatb  30184  cdlemf2  30569  cdlemg2cex  30598  tendodi1  30791  tendodi2  30792  diblss  31178  dihopelvalcpre  31256  dih1dimatlem  31337  dihglblem6  31348
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