Theorem simplll 794

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 472	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	ad2antrr 758	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  simp-4l  802  adant423OLD  819  f1imass  6422  oeeui  7569  oaabs2  7612  boxcutc  7837  omxpenlem  7946  cantnfle  8451  acndom2  8760  infpwfien  8768  sornom  8982  isf32lem2  9059  isf32lem4  9061  fin1a2lem11  9115  ttukeylem5  9218  pwfseq  9365  gchina  9400  inttsk  9475  inar1  9476  prlem936  9748  mulcmpblnr  9771  00id  10090  mul02lem1  10091  addid1  10095  cnegex  10096  negeu  10150  add20  10419  ltmul12a  10758  lediv12a  10795  fiminre  10851  cru  10889  qextltlem  11907  xmullem  11966  xlemul1a  11990  ixxss12  12066  ioodisj  12173  elfz0fzfz0  12313  fsuppmapnn0fz  12658  seqf1o  12704  mulexpz  12762  leexp1a  12781  seqcoll  13105  swrdswrdlem  13311  abs3lem  13926  cau3lem  13942  climcau  14249  sumeq2ii  14271  summolem2  14294  climcndslem1  14420  climcndslem2  14421  geomulcvg  14446  mertenslem1  14455  mertenslem2  14456  mertens  14457  prodeq2ii  14482  prodmolem2  14504  bitsfzo  14995  sadadd2lem2  15010  dvdsmulgcd  15112  qredeu  15210  pc2dvds  15421  pcz  15423  ramcl  15571  firest  15916  mreexexlemd  16127  isacs2  16137  iscatd2  16165  ipodrsima  16988  mrelatlub  17009  mndpropd  17139  mhmeql  17187  isgrpinv  17295  mhmid  17359  mhmmnd  17360  issubg4  17436  gasubg  17558  symgextf  17660  pmtr3ncom  17718  gexdvds  17822  oddvdssubg  18081  cyggeninv  18108  cyggenod  18109  issrg  18330  dvdsrmul1  18476  unitgrp  18490  cntzsubr  18635  islmhm2  18859  lmhmeql  18876  lbspropd  18920  lssacsex  18965  issubassa2  19166  mplbas2  19291  psgndiflemA  19766  isphl  19792  ocvocv  19834  lindfmm  19985  scmatmats  20136  smatvscl  20149  mdetdiag  20224  m2cpmfo  20380  pmatcollpw3fi1lem1  20410  pm2mpf1  20423  pm2mpghm  20440  fvmptnn04if  20473  chfacfscmulfsupp  20483  chfacfpmmulfsupp  20487  neissex  20741  neiptoptop  20745  neiptopnei  20746  restbas  20772  tgrest  20773  restopnb  20789  cnpco  20881  isnrm3  20973  isreg2  20991  iuncon  21041  1stcrest  21066  2ndcctbss  21068  2ndcomap  21071  2ndcsep  21072  dislly  21110  kgencn2  21170  ptbasfi  21194  txhaus  21260  txkgen  21265  txcon  21302  qtopcn  21327  regr1lem2  21353  kqnrmlem1  21356  kqnrmlem2  21357  trfbas2  21457  trfil2  21501  flimcf  21596  hauspwpwf1  21601  fclscf  21639  flimfnfcls  21642  cnextcn  21681  ustexsym  21829  ustex2sym  21830  ustex3sym  21831  ustuqtop4  21858  utop3cls  21865  utopreg  21866  ucnima  21895  ucncn  21899  fmucnd  21906  metequiv2  22125  prdsxmslem2  22144  metcnpi3  22161  metustto  22168  metustid  22169  metustexhalf  22171  ngptgp  22250  xrsblre  22422  icccmp  22436  reconnlem1  22437  reconn  22439  opnreen  22442  metdsf  22459  metdscn  22467  fsumcn  22481  elcncf2  22501  cncfmet  22519  pcoass  22632  lmcau  22919  rrxdstprj1  23000  pmltpc  23026  ivthlem2  23028  ivthlem3  23029  ovollb2  23064  volsup  23131  ioombl1  23137  ioorf  23147  dyadss  23168  dyaddisjlem  23169  dyadmax  23172  volcn  23180  cncombf  23231  mbflimsup  23239  itg2const2  23314  iblss2  23378  cpnord  23504  dvmptfsum  23542  fta1g  23731  plydivex  23856  fta1  23867  aannenlem1  23887  ulmdvlem3  23960  abelthlem8  23997  pilem3  24011  advlogexp  24201  cxpmul2z  24237  atantayl2  24465  jensen  24515  isppw2  24641  lgsqr  24876  lgsqrmodndvds  24878  lgsdchrval  24879  lgsquad3  24912  2sqb  24957  dchrisumlem3  24980  rpvmasum2  25001  mulog2sumlem2  25024  pntrsumbnd2  25056  f1otrg  25551  f1otrge  25552  axsegcon  25607  axeuclidlem  25642  axcontlem9  25652  eengtrkg  25665  nbgraf1olem5  25974  cusgrasize2inds  26005  0wlkon  26077  0trlon  26078  0pthon  26109  3v3e3cycl2  26192  wlkiswwlk1  26218  usg2wotspth  26411  vdiscusgra  26448  iseupa  26492  vdn1frgrav2  26552  vdgn1frgrav2  26553  frgrancvvdeqlem9  26568  frgrawopreg  26576  frghash2spot  26590  numclwlk1lem2foa  26618  numclwlk1lem2fo  26622  frgrareggt1  26643  vacn  26933  smcnlem  26936  0lno  27029  chocunii  27544  occl  27547  5oalem1  27897  3oalem2  27906  unoplin  28163  hmoplin  28185  lnconi  28276  kbass5  28363  mdslmd1lem1  28568  mdslmd1lem2  28569  mdsymlem2  28647  cdj1i  28676  disjabrex  28777  disjabrexf  28778  acunirnmpt  28841  fgreu  28854  xrge0infss  28915  xrofsup  28923  xrge0addgt0  29022  submomnd  29041  submarchi  29071  archiabllem1  29078  archiabllem2a  29079  isarchiofld  29148  locfinreflem  29235  rge0scvg  29323  lmxrge0  29326  lmdvg  29327  qqhval2  29354  esumrnmpt2  29457  esumfsup  29459  esumpcvgval  29467  esumcvg  29475  esumgect  29479  esumiun  29483  sigaclfu2  29511  sigainb  29526  insiga  29527  fiunelros  29564  measinblem  29610  measinb  29611  measdivcstOLD  29614  measdivcst  29615  omssubadd  29689  oddpwdc  29743  dstrvprob  29860  sgnmul  29931  sgnsub  29933  signsply0  29954  signstfvneq0  29975  bnj1408  30358  ptpcon  30469  sconpi1  30475  rescon  30482  cvmliftmolem2  30518  cvmlift2lem12  30550  poseq  30994  ifscgr  31321  cgrxfr  31332  outsideofeu  31408  linethru  31430  neibastop1  31524  dnicn  31652  fin2so  32566  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem28  32607  poimirlem31  32610  mblfinlem2  32617  mblfinlem3  32618  itg2addnclem  32631  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  ssbnd  32757  totbndbnd  32758  prtlem10  33168  lssats  33317  lkrlss  33400  lshpset2N  33424  2dim  33774  islvol5  33883  paddasslem11  34134  pexmidlem8N  34281  ltrnid  34439  idltrn  34454  trlator0  34476  trlnidatb  34482  cdlemf2  34868  cdlemg2cex  34897  tendodi1  35090  tendodi2  35091  diblss  35477  dihopelvalcpre  35555  dih1dimatlem  35636  dihglblem6  35647  mzpsubst  36329  mzpcompact2lem  36332  eldioph2  36343  eldioph2b  36344  diophren  36395  pell14qrexpcl  36449  elpell1qr2  36454  monotoddzzfi  36525  acongtr  36563  acongrep  36565  jm2.19lem4  36577  jm2.26a  36585  jm2.26lem3  36586  jm2.26  36587  isnumbasgrplem2  36693  mendassa  36783  clsk3nimkb  37358  prmunb2  37532  4an4132  37726  fiiuncl  38259  ssinc  38292  ssdec  38293  supxrgelem  38494  infxr  38524  mullimc  38683  mullimcf  38690  neglimc  38714  climleltrp  38743  icccncfext  38773  cncfiooicclem1  38779  fprodcncf  38787  dvnprodlem3  38838  iblcncfioo  38870  itgspltprt  38871  stoweidlem7  38900  stoweidlem28  38921  stoweidlem34  38927  stoweidlem48  38941  stoweidlem52  38945  wallispilem3  38960  fourierdlem12  39012  fourierdlem38  39038  fourierdlem39  39039  fourierdlem42  39042  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem51  39050  fourierdlem65  39064  fourierdlem73  39072  fourierdlem76  39075  fourierdlem87  39086  fourierdlem103  39102  fourierdlem104  39103  sge0f1o  39275  sge0le  39300  sge0reuz  39340  ismeannd  39360  isomenndlem  39420  hoicvr  39438  hoidmvle  39490  smflimlem2  39658  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbnd  40225  cusgrsize2inds  40669  pthdepissPth  40941  usgr2wlkneq  40962  crctcsh1wlkn0  41024  umgr3v3e3cycl  41351  vdgn1frgrv2  41466  frgrwopreg  41486  frgrhash2wsp  41497  av-numclwlk1lem2foa  41521  av-numclwlk1lem2fo  41525  mgmhmeql  41593