Theorem simplll 798

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simplll	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

Proof of Theorem simplll

Step	Hyp	Ref	Expression
1		simpl 473	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ad2antrr 762	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  simp-4l  806  adant423OLD  823  f1imass  6521  oeeui  7682  oaabs2  7725  omxpenlem  8061  cantnfle  8568  acndom2  8877  infpwfien  8885  sornom  9099  isf32lem2  9176  isf32lem4  9178  fin1a2lem11  9232  ttukeylem5  9335  pwfseq  9486  gchina  9521  inttsk  9596  inar1  9597  prlem936  9869  mulcmpblnr  9892  00id  10211  mul02lem1  10212  addid1  10216  cnegex  10217  negeu  10271  add20  10540  ltmul12a  10879  lediv12a  10916  fiminre  10972  cru  11012  qextltlem  12033  xmullem  12094  xlemul1a  12118  ixxss12  12195  ioodisj  12302  elfz0fzfz0  12444  fsuppmapnn0fz  12796  seqf1o  12842  mulexpz  12900  leexp1a  12919  seqcoll  13248  swrdswrdlem  13459  abs3lem  14078  cau3lem  14094  climcau  14401  sumeq2ii  14423  summolem2  14447  climcndslem1  14581  climcndslem2  14582  geomulcvg  14607  mertenslem1  14616  mertenslem2  14617  mertens  14618  prodeq2ii  14643  prodmolem2  14665  bitsfzo  15157  sadadd2lem2  15172  dvdsmulgcd  15274  qredeu  15372  pc2dvds  15583  pcz  15585  ramcl  15733  firest  16093  mreexexlemd  16304  isacs2  16314  iscatd2  16342  ipodrsima  17165  mrelatlub  17186  mndpropd  17316  mhmeql  17364  isgrpinv  17472  mhmid  17536  mhmmnd  17537  issubg4  17613  gasubg  17735  symgextf  17837  pmtr3ncom  17895  gexdvds  17999  oddvdssubg  18258  cyggeninv  18285  cyggenod  18286  issrg  18507  dvdsrmul1  18653  unitgrp  18667  cntzsubr  18812  islmhm2  19038  lmhmeql  19055  lbspropd  19099  lssacsex  19144  issubassa2  19345  mplbas2  19470  psgndiflemA  19947  isphl  19973  ocvocv  20015  lindfmm  20166  scmatmats  20317  smatvscl  20330  mdetdiag  20405  m2cpmfo  20561  pmatcollpw3fi1lem1  20591  pm2mpf1  20604  pm2mpghm  20621  fvmptnn04if  20654  chfacfscmulfsupp  20664  chfacfpmmulfsupp  20668  neissex  20931  neiptoptop  20935  neiptopnei  20936  restbas  20962  tgrest  20963  restopnb  20979  cnpco  21071  isnrm3  21163  isreg2  21181  iunconn  21231  1stcrest  21256  2ndcctbss  21258  2ndcomap  21261  2ndcsep  21262  dislly  21300  kgencn2  21360  ptbasfi  21384  txhaus  21450  txkgen  21455  txconn  21492  qtopcn  21517  regr1lem2  21543  kqnrmlem1  21546  kqnrmlem2  21547  trfbas2  21647  trfil2  21691  flimcf  21786  hauspwpwf1  21791  fclscf  21829  flimfnfcls  21832  cnextcn  21871  ustexsym  22019  ustex2sym  22020  ustex3sym  22021  ustuqtop4  22048  utop3cls  22055  utopreg  22056  ucnima  22085  ucncn  22089  fmucnd  22096  metequiv2  22315  prdsxmslem2  22334  metcnpi3  22351  metustto  22358  metustid  22359  metustexhalf  22361  ngptgp  22440  xrsblre  22614  icccmp  22628  reconnlem1  22629  reconn  22631  opnreen  22634  metdsf  22651  metdscn  22659  fsumcn  22673  elcncf2  22693  cncfmet  22711  pcoass  22824  lmcau  23111  rrxdstprj1  23192  pmltpc  23219  ivthlem2  23221  ivthlem3  23222  ovollb2  23257  volsup  23324  ioombl1  23330  ioorf  23341  dyadss  23362  dyaddisjlem  23363  dyadmax  23366  volcn  23374  cncombf  23425  mbflimsup  23433  itg2const2  23508  iblss2  23572  cpnord  23698  dvmptfsum  23738  fta1g  23927  plydivex  24052  fta1  24063  aannenlem1  24083  ulmdvlem3  24156  abelthlem8  24193  pilem3  24207  advlogexp  24401  cxpmul2z  24437  atantayl2  24665  jensen  24715  isppw2  24841  lgsqr  25076  lgsqrmodndvds  25078  lgsdchrval  25079  lgsquad3  25112  2sqb  25157  dchrisumlem3  25180  rpvmasum2  25201  mulog2sumlem2  25224  pntrsumbnd2  25256  f1otrg  25751  f1otrge  25752  axsegcon  25807  axeuclidlem  25842  axcontlem9  25852  eengtrkg  25865  cusgrsize2inds  26349  pthdepisspth  26631  usgr2wlkneq  26652  crctcshwlkn0  26713  umgr3v3e3cycl  27044  vdgn1frgrv2  27160  frgrwopreglem5  27185  frgrwopreg  27187  frgrhash2wsp  27196  numclwlk1lem2fo  27228  vacn  27549  smcnlem  27552  0lno  27645  chocunii  28160  occl  28163  5oalem1  28513  3oalem2  28522  unoplin  28779  hmoplin  28801  lnconi  28892  kbass5  28979  mdslmd1lem1  29184  mdslmd1lem2  29185  mdsymlem2  29263  cdj1i  29292  disjabrex  29395  disjabrexf  29396  acunirnmpt  29459  fgreu  29471  xrge0infss  29525  xrofsup  29533  fsumiunle  29575  xrge0addgt0  29691  submomnd  29710  submarchi  29740  archiabllem1  29747  archiabllem2a  29748  isarchiofld  29817  locfinreflem  29907  rge0scvg  29995  lmxrge0  29998  lmdvg  29999  qqhval2  30026  esumrnmpt2  30130  esumfsup  30132  esumpcvgval  30140  esumcvg  30148  esumgect  30152  esumiun  30156  sigaclfu2  30184  sigainb  30199  insiga  30200  fiunelros  30237  measinblem  30283  measinb  30284  measdivcstOLD  30287  measdivcst  30288  omssubadd  30362  oddpwdc  30416  dstrvprob  30533  sgnmul  30604  sgnsub  30606  signsply0  30628  signstfvneq0  30649  bnj1408  31104  ptpconn  31215  sconnpi1  31221  resconn  31228  cvmliftmolem2  31264  cvmlift2lem12  31296  poseq  31750  noetalem3  31865  noetalem5  31867  conway  31910  ifscgr  32151  cgrxfr  32162  outsideofeu  32238  linethru  32260  neibastop1  32354  dnicn  32482  fin2so  33396  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem28  33437  poimirlem31  33440  mblfinlem2  33447  mblfinlem3  33448  itg2addnclem  33461  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  ssbnd  33587  totbndbnd  33588  prtlem10  34150  lssats  34299  lkrlss  34382  lshpset2N  34406  2dim  34756  islvol5  34865  paddasslem11  35116  pexmidlem8N  35263  ltrnid  35421  idltrn  35436  trlator0  35458  trlnidatb  35464  cdlemf2  35850  cdlemg2cex  35879  tendodi1  36072  tendodi2  36073  diblss  36459  dihopelvalcpre  36537  dih1dimatlem  36618  dihglblem6  36629  mzpsubst  37311  mzpcompact2lem  37314  eldioph2  37325  eldioph2b  37326  diophren  37377  pell14qrexpcl  37431  elpell1qr2  37436  monotoddzzfi  37507  acongtr  37545  acongrep  37547  jm2.19lem4  37559  jm2.26a  37567  jm2.26lem3  37568  jm2.26  37569  isnumbasgrplem2  37674  mendassa  37764  clsk3nimkb  38338  prmunb2  38510  4an4132  38705  fiiuncl  39234  ssinc  39264  ssdec  39265  supxrgelem  39553  infxr  39583  mullimc  39848  mullimcf  39855  neglimc  39879  climleltrp  39908  climisp  39978  limsupresxr  39998  liminfresxr  39999  liminflimsupclim  40039  icccncfext  40100  cncfiooicclem1  40106  fprodcncf  40114  dvnprodlem3  40163  iblcncfioo  40194  itgspltprt  40195  stoweidlem7  40224  stoweidlem28  40245  stoweidlem34  40251  stoweidlem48  40265  stoweidlem52  40269  wallispilem3  40284  fourierdlem12  40336  fourierdlem38  40362  fourierdlem39  40363  fourierdlem42  40366  fourierdlem46  40369  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem51  40374  fourierdlem65  40388  fourierdlem73  40396  fourierdlem76  40399  fourierdlem87  40410  fourierdlem103  40426  fourierdlem104  40427  sge0f1o  40599  sge0le  40624  sge0reuz  40664  ismeannd  40684  isomenndlem  40744  hoicvr  40762  hoidmvle  40814  smflimlem2  40980  smflimmpt  41016  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbnd  41697  mgmhmeql  41803