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  6085  tfrlem1  6944  oeeui  7150  oaabs2  7193  boxcutc  7415  omxpenlem  7521  cantnfle  7989  cantnfleOLD  8019  acndom2  8334  infpwfien  8342  sornom  8556  isf32lem2  8633  isf32lem4  8635  fin1a2lem11  8689  ttukeylem5  8792  pwfseq  8941  gchina  8976  inttsk  9051  inar1  9052  prlem936  9326  00id  9654  mul02lem1  9655  addid1  9659  cnegex  9660  negeu  9710  add20  9961  ltmul12a  10295  lediv12a  10335  cru  10424  qextltlem  11282  xmullem  11337  xlemul1a  11361  ixxss12  11430  ioodisj  11531  elfz0fzfz0  11601  seqf1o  11963  mulexpz  12020  leexp1a  12038  seqcoll  12333  swrdswrdlem  12470  abs3lem  12943  cau3lem  12959  climcau  13265  sumeq2ii  13287  summolem2  13310  climcndslem1  13429  climcndslem2  13430  geomulcvg  13453  mertenslem1  13461  mertenslem2  13462  mertens  13463  bitsfzo  13748  sadadd2lem2  13763  dvdsmulgcd  13855  qredeu  13910  pc2dvds  14062  pcz  14064  ramcl  14207  firest  14489  mreexexlemd  14700  isacs2  14709  iscatd2  14737  ipodrsima  15453  mrelatlub  15474  mndpropd  15564  mhmeql  15610  isgrpinv  15706  mulgnn0dir  15768  issubg4  15818  gasubg  15938  symgextf  16040  pmtr3ncom  16099  gexdvds  16203  oddvdssubg  16457  cyggeninv  16480  cyggenod  16481  issrg  16730  dvdsrmul1  16867  unitgrp  16881  cntzsubr  17019  islmhm2  17241  lmhmeql  17258  lbspropd  17302  lssacsex  17347  issubassa2  17537  mplbas2  17674  mplbas2OLD  17675  psgndiflemA  18155  isphl  18181  ocvocv  18220  lindfmm  18380  mdetdiag  18536  neissex  18862  neiptoptop  18866  neiptopnei  18867  restbas  18893  tgrest  18894  restopnb  18910  cnpco  19002  isnrm3  19094  isreg2  19112  iuncon  19163  1stcrest  19188  2ndcctbss  19190  2ndcomap  19193  2ndcsep  19194  dislly  19232  kgencn2  19261  ptbasfi  19285  txhaus  19351  txkgen  19356  txcon  19393  qtopcn  19418  regr1lem2  19444  kqnrmlem1  19447  kqnrmlem2  19448  trfbas2  19547  trfil2  19591  flimcf  19686  hauspwpwf1  19691  fclscf  19729  flimfnfcls  19732  cnextcn  19770  ustexsym  19921  ustex2sym  19922  ustex3sym  19923  ustuqtop4  19950  utop3cls  19957  utopreg  19958  ucnima  19987  ucncn  19991  fmucnd  19998  metequiv2  20216  prdsxmslem2  20235  metcnpi3  20252  metusttoOLD  20263  metustto  20264  metustidOLD  20265  metustid  20266  metustexhalfOLD  20269  metustexhalf  20270  ngptgp  20353  xrsblre  20519  icccmp  20533  reconnlem1  20534  reconn  20536  opnreen  20539  metdsf  20555  metdscn  20563  fsumcn  20577  elcncf2  20597  cncfmet  20615  pcoass  20727  lmcau  20954  rrxdstprj1  21039  pmltpc  21065  ivthlem2  21067  ivthlem3  21068  ovollb2  21103  volsup  21169  ioombl1  21175  ioorf  21185  dyadss  21206  dyaddisjlem  21207  dyadmax  21210  volcn  21218  cncombf  21268  mbflimsup  21276  itg2const2  21351  iblss2  21415  cpnord  21541  dvmptfsum  21579  fta1g  21771  plydivex  21895  fta1  21906  aannenlem1  21926  ulmdvlem3  21999  abelthlem8  22036  pilem3  22050  advlogexp  22232  cxpmul2z  22268  atantayl2  22465  jensen  22514  isppw2  22585  lgsqr  22817  lgsdchrval  22818  lgsquad3  22832  2sqb  22849  dchrisumlem3  22872  rpvmasum2  22893  mulog2sumlem2  22916  pntrsumbnd2  22948  f1otrg  23268  f1otrge  23269  axsegcon  23324  axeuclidlem  23359  axcontlem9  23369  eengtrkg  23382  nbgraf1olem5  23505  cusgrasize2inds  23536  0wlkon  23597  0trlon  23598  0pthon  23629  3v3e3cycl2  23701  iseupa  23737  vacn  24240  smcnlem  24243  0lno  24341  chocunii  24855  occl  24858  5oalem1  25208  3oalem2  25217  unoplin  25475  hmoplin  25497  lnconi  25588  kbass5  25675  mdslmd1lem1  25880  mdslmd1lem2  25881  mdsymlem2  25959  cdj1i  25988  disjabrex  26076  disjabrexf  26077  fgreu  26140  xrge0infss  26203  xrofsup  26205  xrge0addgt0  26298  submomnd  26317  submarchi  26347  archiabllem1  26354  archiabllem2a  26355  isarchiofld  26429  rge0scvg  26523  lmxrge0  26526  lmdvg  26527  qqhval2  26555  esumfsup  26663  esumpcvgval  26671  esumcvg  26679  sigaclfu2  26708  sigainb  26723  insiga  26724  measinblem  26778  measinb  26779  measdivcstOLD  26782  measdivcst  26783  oddpwdc  26880  dstrvprob  26997  sgnmul  27068  sgnsub  27070  signsply0  27095  signstfvneq0  27116  ptpcon  27265  sconpi1  27271  rescon  27278  cvmliftmolem2  27314  cvmlift2lem12  27346  prodeq2ii  27569  prodmolem2  27591  poseq  27857  ifscgr  28218  cgrxfr  28229  outsideofeu  28305  linethru  28327  fin2so  28563  mblfinlem2  28576  mblfinlem3  28577  itg2addnclem  28590  ftc1anclem7  28620  ftc1anclem8  28621  ftc1anc  28622  neibastop1  28727  ssbnd  28834  totbndbnd  28835  prtlem10  29157  mzpsubst  29232  mzpcompact2lem  29235  eldioph2  29247  eldioph2b  29248  diophren  29299  pell14qrexpcl  29355  elpell1qr2  29360  monotoddzzfi  29430  acongtr  29468  acongrep  29470  jm2.19lem4  29488  jm2.26a  29496  jm2.26lem3  29497  jm2.26  29498  isnumbasgrplem2  29607  mendassa  29698  stoweidlem7  29949  stoweidlem28  29970  stoweidlem34  29976  stoweidlem48  29990  stoweidlem49  29991  stoweidlem52  29994  stoweidlem57  29999  wallispilem3  30009  ralxfrd2  30284  wlkiswwlk1  30471  usg2wotspth  30550  vdiscusgra  30684  vdn1frgrav2  30765  vdgn1frgrav2  30766  frgrancvvdeqlem9  30781  frgrawopreg  30789  frghash2spot  30803  numclwlk1lem2foa  30831  numclwlk1lem2fo  30835  frgrareggt1  30856  fsuppmapnn0fz  30944  m2cpmfo  31227  pmatcollpw3fi1lem1  31258  pm2mpf1  31271  pm2mpghm  31288  fvmptnn04if  31320  chfacfscmulfsupp  31330  chfacfpmmulfsupp  31334  4animp1  31518  4an4132  31520  bnj1408  32344  lssats  32980  lkrlss  33063  lshpset2N  33087  2dim  33437  islvol5  33546  paddasslem11  33797  pexmidlem8N  33944  ltrnid  34102  idltrn  34117  trlator0  34138  trlnidatb  34144  cdlemf2  34529  cdlemg2cex  34558  tendodi1  34751  tendodi2  34752  diblss  35138  dihopelvalcpre  35216  dih1dimatlem  35297  dihglblem6  35308
  Copyright terms: Public domain W3C validator