Theorem simplll 787

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 743	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  f1imass  7266  poseq  8156  oeeui  8590  oaabs2  8637  naddssim  8674  omxpenlem  9068  findcard3  9245  wemappo  9513  acndom2  10049  infpwfien  10057  sornom  10271  isf32lem2  10348  isf32lem4  10350  fin1a2lem11  10404  pwfseq  10659  gchina  10694  inttsk  10769  inar1  10770  prlem936  11042  mulcmpblnr  11066  00id  11395  mul02lem1  11396  addrid  11400  cnegex  11401  negeu  11457  add20  11736  ltmul12a  12081  lediv12a  12118  cru  12220  qextltlem  13238  xmullem  13300  xlemul1a  13324  ixxss12  13402  ioodisj  13519  elfz0fzfz0  13672  fsuppmapnn0fz  14043  seqf1o  14090  mulexpz  14149  leexp1a  14222  seqcoll  14512  swrdswrdlem  14752  pfxccatin12lem3  14780  sgnsub  15154  sgnmul  15155  abs3lem  15401  cau3lem  15417  climcau  15733  sumeq2ii  15755  climcndslem1  15914  climcndslem2  15915  geomulcvg  15941  mertenslem1  15949  mertenslem2  15950  mertens  15951  prodeq2ii  15976  prodmolem2  16000  bitsfzo  16503  sadadd2lem2  16518  dvdsmulgcd  16624  qredeu  16726  pc2dvds  16949  pcz  16951  ramcl  17099  firest  17495  mreexexlemd  17710  isacs2  17719  iscatd2  17747  ipodrsima  18607  mrelatlub  18628  mgmhmeql  18784  sgrppropd  18799  mndpropd  18827  mhmeql  18895  mhmid  19139  mhmmnd  19140  issubg4  19222  cycsubm  19283  cycsubmcom  19285  gasubg  19382  symgextf  19497  pmtr3ncom  19555  gexdvds  19664  oddvdssubg  19935  imasabl  19956  cyggeninv  19963  cyggenod  19964  submomnd  20212  issrg  20280  dvdsrmul1  20462  unitgrp  20476  cntzsubrng  20681  cntzsubr  20720  islmhm2  21174  lmhmeql  21191  lbspropd  21235  lssacsex  21283  rngqiprngimfo  21456  psgndiflemA  21766  isphl  21793  ocvocv  21836  lindfmm  21992  issubassa2  22057  mplbas2  22208  scmatmats  22683  smatvscl  22696  mdetdiag  22771  m2cpmfo  22928  pmatcollpw3fi1lem1  22958  pm2mpf1  22971  pm2mpghm  22988  fvmptnn04if  23021  chfacfscmulfsupp  23031  chfacfpmmulfsupp  23035  neissex  23299  neiptoptop  23303  neiptopnei  23304  restbas  23330  tgrest  23331  restopnb  23347  cnpco  23439  isreg2  23549  iunconn  23600  1stcrest  23625  2ndcctbss  23627  2ndcomap  23630  2ndcsep  23631  dislly  23669  kgencn2  23729  ptbasfi  23753  txhaus  23819  txkgen  23824  txconn  23861  qtopcn  23886  regr1lem2  23912  kqnrmlem1  23915  kqnrmlem2  23916  trfbas2  24015  trfil2  24059  flimcf  24154  hauspwpwf1  24159  fclscf  24197  flimfnfcls  24200  ustexsym  24388  ustuqtop4  24416  utop3cls  24423  utopreg  24424  ucnima  24452  ucncn  24456  metequiv2  24682  prdsxmslem2  24701  metcnpi3  24718  metustto  24725  metustid  24726  metustexhalf  24728  ngptgp  24808  xrsblre  24984  icccmp  24998  reconnlem1  24999  reconn  25001  opnreen  25004  metdsf  25021  metdscn  25029  mpomulcn  25041  fsumcn  25044  elcncf2  25064  cncfmet  25083  pcoass  25198  lmcau  25487  rrxdstprj1  25583  pmltpc  25624  ivthlem2  25626  ivthlem3  25627  ovollb2  25663  volsup  25730  ioombl1  25736  ioorf  25747  dyadss  25768  dyaddisjlem  25769  dyadmax  25772  volcn  25780  cncombf  25832  mbflimsup  25840  itg2const2  25915  iblss2  25980  cpnord  26109  dvmptfsum  26149  fta1g  26342  plydivex  26473  fta1  26484  aannenlem1  26506  ulmdvlem3  26580  advlogexp  26835  cxpmul2z  26871  atantayl2  27118  jensen  27168  isppw2  27294  lgsqr  27530  lgsqrmodndvds  27532  lgsdchrval  27533  lgsquad3  27566  2sqb  27611  dchrisumlem3  27670  pntrsumbnd2  27746  noinfbnd1lem5  27906  noetasuplem4  27915  noetainflem4  27919  noetalem1  27920  conway  27987  eqcuts3  28012  madebdayim  28096  madebdaylemlrcut  28107  negsprop  28243  mulscom  28347  absmuls  28452  bdayons  28484  addonbday  28487  bdayfinbndlem1  28675  remulscl  28710  tgjustf  28757  axsegcon  29292  axeuclidlem  29327  axcontlem9  29337  eengtrkg  29351  cusgrsize2inds  29818  pthdepisspth  30099  usgr2wlkneq  30120  crctcshwlkn0  30185  wpthswwlks2on  30328  clwwlkccatlem  30355  wwlksext2clwwlk  30423  umgr3v3e3cycl  30550  vdgn1frgrv2  30662  frgrwopreglem5  30687  frgrwopreg  30689  frgrhash2wsp  30698  numclwwlk1lem2fo  30724  vacn  31061  smcnlem  31064  0lno  31157  chocunii  31668  occl  31671  5oalem1  32021  3oalem2  32030  unoplin  32287  hmoplin  32309  lnconi  32400  kbass5  32487  mdslmd1lem1  32692  mdslmd1lem2  32693  mdsymlem2  32771  cdj1i  32800  opreu2reuALT  32838  unidifsnne  32897  disjabrex  32942  disjabrexf  32943  acunirnmpt  33019  fgreu  33031  suppovss  33041  xrge0infss  33120  xrofsup  33127  fsumiunle  33188  mgcf1o  33336  xrge0addgt0  33350  fzto1st1  33435  cyc3genpm  33485  cycpmgcl  33486  submarchi  33519  archiabllem1  33526  archiabllem2a  33527  isarchiofld  33532  rlocval  33592  imaslmod  33686  lindfpropd  33708  unitprodclb  33715  elrspunidl  33749  drnglring  33795  dflring3  33800  dfufd2lem  33852  mplmulmvr  33942  lvecdim0  34010  constrmon  34147  constrextdg2  34152  locfinreflem  34243  zarcmplem  34284  rge0scvg  34352  lmxrge0  34355  lmdvg  34356  qqhval2  34385  esumrnmpt2  34471  esumfsup  34473  esumpcvgval  34481  esumcvg  34489  esumgect  34493  esumiun  34497  sigaclfu2  34524  sigainb  34539  insiga  34540  fiunelros  34577  measinblem  34623  measinb  34624  measdivcst  34627  measdivcstALTV  34628  omssubadd  34703  oddpwdc  34757  dstrvprob  34875  signsply0  34951  signstfvneq0  34972  bnj1408  35437  ptpconn  35737  sconnpi1  35743  resconn  35750  cvmliftmolem2  35786  cvmlift2lem12  35818  satfsschain  35868  satffunlem2lem1  35908  ifscgr  36548  cgrxfr  36559  outsideofeu  36635  linethru  36657  nmulcom  36698  nmuladdss  36717  neibastop1  36902  dnicn  37113  irrdifflemf  38001  irrdiff  38002  fin2so  38290  matunitlindflem1  38299  matunitlindflem2  38300  poimirlem28  38331  poimirlem31  38334  mblfinlem2  38341  mblfinlem3  38342  itg2addnclem  38354  ftc1anclem7  38382  ftc1anclem8  38383  ftc1anc  38384  ssbnd  38471  totbndbnd  38472  prtlem10  39671  lssats  39818  lkrlss  39901  lshpset2N  39925  2dim  40276  islvol5  40385  paddasslem11  40636  pexmidlem8N  40783  ltrnid  40941  idltrn  40956  trlator0  40977  trlnidatb  40983  cdlemf2  41368  cdlemg2cex  41397  tendodi1  41590  tendodi2  41591  diblss  41976  dihopelvalcpre  42054  dih1dimatlem  42135  dihglblem6  42146  primrootscoprmpow  42898  posbezout  42899  aks6d1c4  42923  sticksstones22  42967  aks6d1c6isolem1  42973  aks6d1c6isolem2  42974  aks6d1c6lem5  42976  grpods  42993  unitscyglem3  42996  unitscyglem4  42997  remul01  43200  sn-subeu  43220  sn-0tie0  43257  prjspertr  43369  prjspersym  43371  0prjspnrel  43391  mzpsubst  43511  mzpcompact2lem  43514  eldioph2  43525  eldioph2b  43526  diophren  43572  pell14qrexpcl  43626  elpell1qr2  43631  monotoddzzfi  43701  acongtr  43737  acongrep  43739  jm2.19lem4  43751  jm2.26a  43759  jm2.26lem3  43760  jm2.26  43761  isnumbasgrplem2  43863  mendassa  43949  omord2lim  44059  cantnftermord  44079  tfsconcatfv1  44098  tfsconcatfv2  44099  naddcnffo  44123  naddcnfcom  44125  naddcnfid1  44126  naddgeoa  44153  clsk3nimkb  44798  prmunb2  45053  4an4132  45240  fiiuncl  45817  ssinc  45837  ssdec  45838  supxrgelem  46085  infxr  46114  cvgcaule  46237  mullimc  46364  mullimcf  46371  neglimc  46393  climleltrp  46422  climisp  46492  limsupresxr  46512  liminfresxr  46513  liminflimsupclim  46553  xlimliminflimsup  46608  icccncfext  46633  cncfiooicclem1  46639  fprodcncf  46646  dvnprodlem3  46694  iblcncfioo  46724  itgspltprt  46725  stoweidlem7  46753  stoweidlem28  46774  stoweidlem34  46780  stoweidlem48  46794  stoweidlem52  46798  wallispilem3  46813  fourierdlem12  46865  fourierdlem38  46891  fourierdlem39  46892  fourierdlem42  46895  fourierdlem46  46898  fourierdlem48  46900  fourierdlem49  46901  fourierdlem50  46902  fourierdlem51  46903  fourierdlem65  46917  fourierdlem73  46925  fourierdlem76  46928  fourierdlem87  46939  fourierdlem103  46955  fourierdlem104  46956  sge0f1o  47128  sge0le  47153  sge0reuz  47193  ismeannd  47213  isomenndlem  47276  hoicvr  47294  hoidmvle  47346  smflimlem2  47518  smflimmpt  47556  fsupdm  47588  finfdm  47592  nndivides2  48153  imasetpreimafvbijlemf1  48185  nnsum4primeseven  48597  nnsum4primesevenALTV  48598  bgoldbtbndlem2  48603  bgoldbtbndlem3  48604  bgoldbtbnd  48606  isubgr3stgrlem6  48768  rrxlinec  49548  iccdisj  49708  upfval  49986  fullthinc  50260