Theorem simplll 786

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) (Proof shortened by Wolf Lammen, 6-Apr-2022.)

Assertion

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

Proof of Theorem simplll

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad3antrrr 742	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  f1imass  7252  poseq  8142  oeeui  8576  oaabs2  8623  naddssim  8660  omxpenlem  9054  findcard3  9231  wemappo  9499  acndom2  10026  infpwfien  10034  sornom  10249  isf32lem2  10326  isf32lem4  10328  fin1a2lem11  10382  pwfseq  10637  gchina  10672  inttsk  10747  inar1  10748  prlem936  11020  mulcmpblnr  11044  00id  11373  mul02lem1  11374  addrid  11378  cnegex  11379  negeu  11435  add20  11714  ltmul12a  12059  lediv12a  12096  cru  12198  qextltlem  13216  xmullem  13278  xlemul1a  13302  ixxss12  13380  ioodisj  13497  elfz0fzfz0  13649  fsuppmapnn0fz  14020  seqf1o  14067  mulexpz  14126  leexp1a  14199  seqcoll  14489  swrdswrdlem  14729  pfxccatin12lem3  14757  sgnsub  15131  sgnmul  15132  abs3lem  15378  cau3lem  15394  climcau  15710  sumeq2ii  15732  climcndslem1  15891  climcndslem2  15892  geomulcvg  15918  mertenslem1  15926  mertenslem2  15927  mertens  15928  prodeq2ii  15953  prodmolem2  15977  bitsfzo  16481  sadadd2lem2  16496  dvdsmulgcd  16602  qredeu  16704  pc2dvds  16927  pcz  16929  ramcl  17077  firest  17473  mreexexlemd  17688  isacs2  17697  iscatd2  17725  ipodrsima  18585  mrelatlub  18606  mgmhmeql  18762  sgrppropd  18777  mndpropd  18805  mhmeql  18873  mhmid  19117  mhmmnd  19118  issubg4  19200  cycsubm  19261  cycsubmcom  19263  gasubg  19360  symgextf  19475  pmtr3ncom  19533  gexdvds  19642  oddvdssubg  19913  imasabl  19934  cyggeninv  19941  cyggenod  19942  submomnd  20190  issrg  20258  dvdsrmul1  20439  unitgrp  20453  cntzsubrng  20640  cntzsubr  20679  islmhm2  21125  lmhmeql  21142  lbspropd  21186  lssacsex  21234  rngqiprngimfo  21400  psgndiflemA  21708  isphl  21735  ocvocv  21778  lindfmm  21934  issubassa2  21999  mplbas2  22150  scmatmats  22625  smatvscl  22638  mdetdiag  22713  m2cpmfo  22870  pmatcollpw3fi1lem1  22900  pm2mpf1  22913  pm2mpghm  22930  fvmptnn04if  22963  chfacfscmulfsupp  22973  chfacfpmmulfsupp  22977  neissex  23241  neiptoptop  23245  neiptopnei  23246  restbas  23272  tgrest  23273  restopnb  23289  cnpco  23381  isreg2  23491  iunconn  23542  1stcrest  23567  2ndcctbss  23569  2ndcomap  23572  2ndcsep  23573  dislly  23611  kgencn2  23671  ptbasfi  23695  txhaus  23761  txkgen  23766  txconn  23803  qtopcn  23828  regr1lem2  23854  kqnrmlem1  23857  kqnrmlem2  23858  trfbas2  23957  trfil2  24001  flimcf  24096  hauspwpwf1  24101  fclscf  24139  flimfnfcls  24142  ustexsym  24330  ustuqtop4  24358  utop3cls  24365  utopreg  24366  ucnima  24394  ucncn  24398  metequiv2  24624  prdsxmslem2  24643  metcnpi3  24660  metustto  24667  metustid  24668  metustexhalf  24670  ngptgp  24750  xrsblre  24926  icccmp  24940  reconnlem1  24941  reconn  24943  opnreen  24946  metdsf  24963  metdscn  24971  mpomulcn  24983  fsumcn  24986  elcncf2  25006  cncfmet  25025  pcoass  25140  lmcau  25429  rrxdstprj1  25525  pmltpc  25566  ivthlem2  25568  ivthlem3  25569  ovollb2  25605  volsup  25672  ioombl1  25678  ioorf  25689  dyadss  25710  dyaddisjlem  25711  dyadmax  25714  volcn  25722  cncombf  25774  mbflimsup  25782  itg2const2  25857  iblss2  25922  cpnord  26051  dvmptfsum  26091  fta1g  26284  plydivex  26415  fta1  26426  aannenlem1  26446  ulmdvlem3  26519  advlogexp  26774  cxpmul2z  26810  atantayl2  27057  jensen  27107  isppw2  27233  lgsqr  27469  lgsqrmodndvds  27471  lgsdchrval  27472  lgsquad3  27505  2sqb  27550  dchrisumlem3  27609  pntrsumbnd2  27685  noinfbnd1lem5  27845  noetasuplem4  27854  noetainflem4  27858  noetalem1  27859  conway  27926  eqcuts3  27951  madebdayim  28035  madebdaylemlrcut  28046  negsprop  28182  mulscom  28286  absmuls  28391  bdayons  28423  addonbday  28426  bdayfinbndlem1  28614  remulscl  28649  tgjustf  28696  axsegcon  29182  axeuclidlem  29217  axcontlem9  29227  eengtrkg  29241  cusgrsize2inds  29708  pthdepisspth  29989  usgr2wlkneq  30010  crctcshwlkn0  30075  wpthswwlks2on  30218  clwwlkccatlem  30245  wwlksext2clwwlk  30313  umgr3v3e3cycl  30440  vdgn1frgrv2  30552  frgrwopreglem5  30577  frgrwopreg  30579  frgrhash2wsp  30588  numclwwlk1lem2fo  30614  vacn  30951  smcnlem  30954  0lno  31047  chocunii  31558  occl  31561  5oalem1  31911  3oalem2  31920  unoplin  32177  hmoplin  32199  lnconi  32290  kbass5  32377  mdslmd1lem1  32582  mdslmd1lem2  32583  mdsymlem2  32661  cdj1i  32690  opreu2reuALT  32729  unidifsnne  32788  disjabrex  32833  disjabrexf  32834  acunirnmpt  32912  fgreu  32924  suppovss  32934  xrge0infss  33013  xrofsup  33020  fsumiunle  33081  mgcf1o  33231  xrge0addgt0  33245  fzto1st1  33330  cyc3genpm  33380  cycpmgcl  33381  submarchi  33414  archiabllem1  33421  archiabllem2a  33422  isarchiofld  33427  rlocval  33487  imaslmod  33583  lindfpropd  33606  unitprodclb  33613  elrspunidl  33647  drnglring  33694  dflring3  33699  dfufd2lem  33751  mplmulmvr  33841  lvecdim0  33909  constrmon  34046  constrextdg2  34051  locfinreflem  34142  zarcmplem  34183  rge0scvg  34251  lmxrge0  34254  lmdvg  34255  qqhval2  34284  esumrnmpt2  34370  esumfsup  34372  esumpcvgval  34380  esumcvg  34388  esumgect  34392  esumiun  34396  sigaclfu2  34423  sigainb  34438  insiga  34439  fiunelros  34476  measinblem  34522  measinb  34523  measdivcst  34526  measdivcstALTV  34527  omssubadd  34602  oddpwdc  34656  dstrvprob  34774  signsply0  34850  signstfvneq0  34871  bnj1408  35336  ptpconn  35591  sconnpi1  35597  resconn  35604  cvmliftmolem2  35640  cvmlift2lem12  35672  satfsschain  35722  satffunlem2lem1  35762  ifscgr  36402  cgrxfr  36413  outsideofeu  36489  linethru  36511  nmulcom  36552  neibastop1  36727  dnicn  36938  irrdifflemf  37824  irrdiff  37825  fin2so  38113  matunitlindflem1  38122  matunitlindflem2  38123  poimirlem28  38154  poimirlem31  38157  mblfinlem2  38164  mblfinlem3  38165  itg2addnclem  38177  ftc1anclem7  38205  ftc1anclem8  38206  ftc1anc  38207  ssbnd  38294  totbndbnd  38295  prtlem10  39496  lssats  39643  lkrlss  39726  lshpset2N  39750  2dim  40101  islvol5  40210  paddasslem11  40461  pexmidlem8N  40608  ltrnid  40766  idltrn  40781  trlator0  40802  trlnidatb  40808  cdlemf2  41193  cdlemg2cex  41222  tendodi1  41415  tendodi2  41416  diblss  41801  dihopelvalcpre  41879  dih1dimatlem  41960  dihglblem6  41971  primrootscoprmpow  42723  posbezout  42724  aks6d1c4  42748  sticksstones22  42792  aks6d1c6isolem1  42798  aks6d1c6isolem2  42799  aks6d1c6lem5  42801  grpods  42818  unitscyglem3  42821  unitscyglem4  42822  remul01  43023  sn-subeu  43043  sn-0tie0  43080  prjspertr  43194  prjspersym  43196  0prjspnrel  43216  mzpsubst  43336  mzpcompact2lem  43339  eldioph2  43350  eldioph2b  43351  diophren  43397  pell14qrexpcl  43451  elpell1qr2  43456  monotoddzzfi  43526  acongtr  43562  acongrep  43564  jm2.19lem4  43576  jm2.26a  43584  jm2.26lem3  43585  jm2.26  43586  isnumbasgrplem2  43688  mendassa  43774  omord2lim  43884  cantnftermord  43904  tfsconcatfv1  43923  tfsconcatfv2  43924  naddcnffo  43948  naddcnfcom  43950  naddcnfid1  43951  naddgeoa  43978  clsk3nimkb  44623  prmunb2  44880  4an4132  45067  fiiuncl  45644  ssinc  45664  ssdec  45665  supxrgelem  45912  infxr  45941  cvgcaule  46064  mullimc  46191  mullimcf  46198  neglimc  46220  climleltrp  46249  climisp  46319  limsupresxr  46339  liminfresxr  46340  liminflimsupclim  46380  xlimliminflimsup  46435  icccncfext  46460  cncfiooicclem1  46466  fprodcncf  46473  dvnprodlem3  46521  iblcncfioo  46551  itgspltprt  46552  stoweidlem7  46580  stoweidlem28  46601  stoweidlem34  46607  stoweidlem48  46621  stoweidlem52  46625  wallispilem3  46640  fourierdlem12  46692  fourierdlem38  46718  fourierdlem39  46719  fourierdlem42  46722  fourierdlem46  46725  fourierdlem48  46727  fourierdlem49  46728  fourierdlem50  46729  fourierdlem51  46730  fourierdlem65  46744  fourierdlem73  46752  fourierdlem76  46755  fourierdlem87  46766  fourierdlem103  46782  fourierdlem104  46783  sge0f1o  46955  sge0le  46980  sge0reuz  47020  ismeannd  47040  isomenndlem  47103  hoicvr  47121  hoidmvle  47173  smflimlem2  47345  smflimmpt  47383  fsupdm  47415  finfdm  47419  nndivides2  47977  imasetpreimafvbijlemf1  48009  nnsum4primeseven  48421  nnsum4primesevenALTV  48422  bgoldbtbndlem2  48427  bgoldbtbndlem3  48428  bgoldbtbnd  48430  isubgr3stgrlem6  48592  rrxlinec  49368  iccdisj  49528  upfval  49806  fullthinc  50080