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  7260  poseq  8159  oeeui  8595  oaabs2  8642  naddssim  8679  omxpenlem  9081  findcard3  9258  wemappo  9527  acndom2  10114  infpwfien  10122  sornom  10336  isf32lem2  10413  isf32lem4  10415  fin1a2lem11  10469  pwfseq  10730  gchina  10765  inttsk  10840  inar1  10841  prlem936  11113  mulcmpblnr  11137  00id  11466  mul02lem1  11467  addrid  11471  cnegex  11472  negeu  11528  add20  11809  ltmul12a  12154  lediv12a  12191  cru  12293  qextltlem  13313  xmullem  13375  xlemul1a  13399  ixxss12  13477  ioodisj  13594  elfz0fzfz0  13747  fsuppmapnn0fz  14119  seqf1o  14166  mulexpz  14225  leexp1a  14298  seqcoll  14589  swrdswrdlem  14833  pfxccatin12lem3  14861  s3rex  15081  sgnsub  15239  sgnmul  15240  abs3lem  15486  cau3lem  15502  climcau  15818  sumeq2ii  15840  climcndslem1  15998  climcndslem2  15999  geomulcvg  16025  mertenslem1  16033  mertenslem2  16034  mertens  16035  prodeq2ii  16060  prodmolem2  16082  bitsfzo  16585  sadadd2lem2  16600  dvdsmulgcd  16710  qredeu  16813  pc2dvds  17037  pcz  17039  ramcl  17187  firest  17583  mreexexlemd  17798  isacs2  17807  iscatd2  17835  ipodrsima  18695  mrelatlub  18716  mgmhmeql  18885  sgrppropd  18900  mndpropd  18931  mhmeql  19002  mhmid  19253  mhmmnd  19254  issubg4  19336  cycsubm  19397  cycsubmcom  19399  gasubg  19496  symgextf  19611  pmtr3ncom  19669  gexdvds  19778  oddvdssubg  20049  imasabl  20070  cyggeninv  20077  cyggenod  20078  submomnd  20326  issrg  20394  dvdsrmul1  20579  unitgrp  20593  cntzsubrng  20799  cntzsubr  20838  islmhm2  21293  lmhmeql  21310  lbspropd  21354  lssacsex  21402  rngqiprngimfo  21577  psgndiflemA  21887  isphl  21914  ocvocv  21957  lindfmm  22113  issubassa2  22180  mplbas2  22331  scmatmats  22806  smatvscl  22819  mdetdiag  22894  matunitlindflem1  22974  matunitlindflem2  22975  m2cpmfo  23054  pmatcollpw3fi1lem1  23084  pm2mpf1  23097  pm2mpghm  23114  fvmptnn04if  23147  chfacfscmulfsupp  23157  chfacfpmmulfsupp  23161  neissex  23425  neiptoptop  23429  neiptopnei  23430  restbas  23456  tgrest  23457  restopnb  23473  cnpco  23565  isreg2  23675  iunconn  23726  1stcrest  23751  2ndcctbss  23754  2ndcomap  23757  2ndcsep  23758  dislly  23796  kgencn2  23856  ptbasfi  23880  txhaus  23946  txkgen  23951  txconn  23988  qtopcn  24013  regr1lem2  24039  kqnrmlem1  24042  kqnrmlem2  24043  trfbas2  24142  trfil2  24186  flimcf  24281  hauspwpwf1  24286  fclscf  24324  flimfnfcls  24327  ustexsym  24515  ustuqtop4  24543  utop3cls  24550  utopreg  24551  ucnima  24579  ucncn  24583  metequiv2  24809  prdsxmslem2  24828  metcnpi3  24845  metustto  24852  metustid  24853  metustexhalf  24855  ngptgp  24935  xrsblre  25111  icccmp  25125  reconnlem1  25126  reconn  25128  opnreen  25131  metdsf  25148  metdscn  25156  mpomulcn  25168  fsumcn  25171  elcncf2  25191  cncfmet  25210  pcoass  25325  lmcau  25614  rrxdstprj1  25710  pmltpc  25751  ivthlem2  25753  ivthlem3  25754  ovollb2  25790  volsup  25857  ioombl1  25863  ioorf  25874  dyadss  25895  dyaddisjlem  25896  dyadmax  25899  volcn  25907  cncombf  25959  mbflimsup  25967  itg2const2  26042  iblss2  26106  cpnord  26235  dvmptfsum  26275  fta1g  26468  plydivex  26600  fta1  26611  aannenlem1  26637  ulmdvlem3  26711  advlogexp  26965  cxpmul2z  27001  atantayl2  27248  jensen  27298  isppw2  27424  lgsqr  27660  lgsqrmodndvds  27662  lgsdchrval  27663  lgsquad3  27696  2sqb  27741  dchrisumlem3  27800  pntrsumbnd2  27876  noinfbnd1lem5  28066  noetasuplem4  28075  noetainflem4  28079  noetalem1  28080  conway  28147  eqcuts3  28172  madebdayim  28256  madebdaylemlrcut  28267  negsprop  28403  mulscom  28507  absmuls  28612  bdayons  28644  addonbday  28647  bdayfinbndlem1  28835  remulscl  28870  tgjustf  28917  axsegcon  29487  axeuclidlem  29522  axcontlem9  29532  eengtrkg  29546  cusgrsize2inds  30016  pthdepisspth  30303  usgr2wlkneq  30324  crctcshwlkn0  30392  wpthswwlks2on  30535  clwwlkccatlem  30562  wwlksext2clwwlk  30630  umgr3v3e3cycl  30767  vdgn1frgrv2  30879  frgrwopreglem5  30904  frgrwopreg  30906  frgrhash2wsp  30915  numclwwlk1lem2fo  30941  vacn  31278  smcnlem  31281  0lno  31374  chocunii  31885  occl  31888  5oalem1  32238  3oalem2  32247  unoplin  32504  hmoplin  32526  lnconi  32617  kbass5  32704  mdslmd1lem1  32909  mdslmd1lem2  32910  mdsymlem2  32988  cdj1i  33017  opreu2reuALT  33055  unidifsnne  33114  disjabrex  33158  disjabrexf  33159  acunirnmpt  33235  fgreu  33247  suppovss  33256  xrge0infss  33334  xrofsup  33341  fsumiunle  33402  mgcf1o  33546  xrge0addgt0  33560  fzto1st1  33645  cyc3genpm  33695  cycpmgcl  33696  submarchi  33729  archiabllem1  33736  archiabllem2a  33737  isarchiofld  33742  rlocval  33802  imaslmod  33896  lindfpropd  33919  unitprodclb  33926  elrspunidl  33960  drnglring  34006  dflring3  34011  dfufd2lem  34063  mplmulmvr  34153  lvecdim0  34221  constrmon  34358  constrextdg2  34363  locfinreflem  34454  zarcmplem  34495  rge0scvg  34563  lmxrge0  34566  lmdvg  34567  qqhval2  34596  esumrnmpt2  34682  esumfsup  34684  esumpcvgval  34692  esumcvg  34700  esumgect  34704  esumiun  34708  sigaclfu2  34735  sigainb  34751  insiga  34752  fiunelros  34789  measinblem  34835  measinb  34836  measdivcst  34839  measdivcstALTV  34840  omssubadd  34915  oddpwdc  34969  dstrvprob  35087  signsply0  35163  signstfvneq0  35184  bnj1408  35649  ptpconn  35967  sconnpi1  35973  resconn  35980  cvmliftmolem2  36016  cvmlift2lem12  36048  satfsschain  36098  satffunlem2lem1  36138  ifscgr  36779  cgrxfr  36790  outsideofeu  36866  linethru  36888  nmulcom  36913  nmuladdss  36932  neibastop1  37117  dnicn  37328  irrdifflemf  38214  irrdiff  38215  fin2so  38498  poimirlem28  38534  poimirlem31  38537  mblfinlem2  38544  mblfinlem3  38545  itg2addnclem  38557  ftc1anclem7  38585  ftc1anclem8  38586  ftc1anc  38587  ssbnd  38690  totbndbnd  38691  prtlem10  39890  lssats  40037  lkrlss  40120  lshpset2N  40144  2dim  40495  islvol5  40604  paddasslem11  40855  pexmidlem8N  41002  ltrnid  41160  idltrn  41175  trlator0  41196  trlnidatb  41202  cdlemf2  41587  cdlemg2cex  41616  tendodi1  41809  tendodi2  41810  diblss  42195  dihopelvalcpre  42273  dih1dimatlem  42354  dihglblem6  42365  primrootscoprmpow  43117  posbezout  43118  aks6d1c4  43142  sticksstones22  43186  aks6d1c6isolem1  43192  aks6d1c6isolem2  43193  aks6d1c6lem5  43195  grpods  43212  unitscyglem3  43215  unitscyglem4  43216  remul01  43426  sn-subeu  43446  sn-0tie0  43483  prjspertr  43595  prjspersym  43597  0prjspnrel  43617  mzpsubst  43712  mzpcompact2lem  43715  eldioph2  43726  eldioph2b  43727  diophren  43773  pell14qrexpcl  43827  elpell1qr2  43832  monotoddzzfi  43902  acongtr  43938  acongrep  43940  jm2.19lem4  43952  jm2.26a  43960  jm2.26lem3  43961  jm2.26  43962  isnumbasgrplem2  44064  mendassa  44150  omord2lim  44260  cantnftermord  44280  tfsconcatfv1  44299  tfsconcatfv2  44300  naddcnffo  44324  naddcnfcom  44326  naddcnfid1  44327  naddgeoa  44354  clsk3nimkb  44999  prmunb2  45254  4an4132  45441  fiiuncl  46025  ssinc  46045  ssdec  46046  supxrgelem  46293  infxr  46322  cvgcaule  46445  mullimc  46572  mullimcf  46579  neglimc  46601  climleltrp  46630  climisp  46700  limsupresxr  46720  liminfresxr  46721  liminflimsupclim  46761  xlimliminflimsup  46816  icccncfext  46841  cncfiooicclem1  46847  fprodcncf  46854  dvnprodlem3  46902  iblcncfioo  46932  itgspltprt  46933  stoweidlem7  46961  stoweidlem28  46982  stoweidlem34  46988  stoweidlem48  47002  stoweidlem52  47006  wallispilem3  47021  fourierdlem12  47073  fourierdlem38  47099  fourierdlem39  47100  fourierdlem42  47103  fourierdlem46  47106  fourierdlem48  47108  fourierdlem49  47109  fourierdlem50  47110  fourierdlem51  47111  fourierdlem65  47125  fourierdlem73  47133  fourierdlem76  47136  fourierdlem87  47147  fourierdlem103  47163  fourierdlem104  47164  sge0f1o  47336  sge0le  47361  sge0reuz  47401  ismeannd  47421  isomenndlem  47484  hoicvr  47502  hoidmvle  47554  smflimlem2  47726  smflimmpt  47764  fsupdm  47796  finfdm  47800  nndivides2  48398  imasetpreimafvbijlemf1  48430  nnsum4primeseven  48842  nnsum4primesevenALTV  48843  bgoldbtbndlem2  48848  bgoldbtbndlem3  48849  bgoldbtbnd  48851  isubgr3stgrlem6  49013  rrxlinec  49792  iccdisj  49950  upfval  50228  fullthinc  50502