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  7294  poseq  8205  oeeui  8642  oaabs2  8689  naddssim  8726  omxpenlem  9128  findcard3  9305  wemappo  9573  acndom2  10163  infpwfien  10171  sornom  10385  isf32lem2  10462  isf32lem4  10464  fin1a2lem11  10518  pwfseq  10779  gchina  10814  inttsk  10889  inar1  10890  prlem936  11162  mulcmpblnr  11186  00id  11515  mul02lem1  11516  addrid  11520  cnegex  11521  negeu  11577  add20  11858  ltmul12a  12203  lediv12a  12240  cru  12342  qextltlem  13362  xmullem  13424  xlemul1a  13448  ixxss12  13526  ioodisj  13643  elfz0fzfz0  13797  fsuppmapnn0fz  14169  seqf1o  14216  mulexpz  14275  leexp1a  14348  seqcoll  14639  swrdswrdlem  14884  pfxccatin12lem3  14912  s3rex  15133  sgnsub  15291  sgnmul  15292  abs3lem  15538  cau3lem  15554  climcau  15870  sumeq2ii  15892  climcndslem1  16050  climcndslem2  16051  geomulcvg  16077  mertenslem1  16085  mertenslem2  16086  mertens  16087  prodeq2ii  16112  prodmolem2  16134  bitsfzo  16637  sadadd2lem2  16652  dvdsmulgcd  16762  qredeu  16865  pc2dvds  17089  pcz  17091  ramcl  17239  firest  17635  mreexexlemd  17850  isacs2  17859  iscatd2  17887  ipodrsima  18747  mrelatlub  18768  mgmhmeql  18937  sgrppropd  18952  mndpropd  18983  mhmeql  19054  mhmid  19305  mhmmnd  19306  issubg4  19388  cycsubm  19449  cycsubmcom  19451  gasubg  19549  symgextf  19664  pmtr3ncom  19722  gexdvds  19831  oddvdssubg  20102  imasabl  20123  cyggeninv  20130  cyggenod  20131  submomnd  20379  issrg  20447  dvdsrmul1  20632  unitgrp  20646  cntzsubrng  20852  cntzsubr  20891  islmhm2  21346  lmhmeql  21363  lbspropd  21407  lssacsex  21455  rngqiprngimfo  21630  psgndiflemA  21940  isphl  21967  ocvocv  22010  lindfmm  22166  issubassa2  22233  mplbas2  22384  scmatmats  22859  smatvscl  22872  mdetdiag  22947  matunitlindflem1  23027  matunitlindflem2  23028  m2cpmfo  23107  pmatcollpw3fi1lem1  23137  pm2mpf1  23150  pm2mpghm  23167  fvmptnn04if  23200  chfacfscmulfsupp  23210  chfacfpmmulfsupp  23214  neissex  23478  neiptoptop  23482  neiptopnei  23483  restbas  23509  tgrest  23510  restopnb  23526  cnpco  23618  isreg2  23728  iunconn  23779  1stcrest  23804  2ndcctbss  23807  2ndcomap  23810  2ndcsep  23811  dislly  23849  kgencn2  23909  ptbasfi  23933  txhaus  23999  txkgen  24004  txconn  24041  qtopcn  24066  regr1lem2  24092  kqnrmlem1  24095  kqnrmlem2  24096  trfbas2  24195  trfil2  24239  flimcf  24334  hauspwpwf1  24339  fclscf  24377  flimfnfcls  24380  ustexsym  24568  ustuqtop4  24596  utop3cls  24603  utopreg  24604  ucnima  24632  ucncn  24636  metequiv2  24862  prdsxmslem2  24881  metcnpi3  24898  metustto  24905  metustid  24906  metustexhalf  24908  ngptgp  24988  xrsblre  25164  icccmp  25178  reconnlem1  25179  reconn  25181  opnreen  25184  metdsf  25201  metdscn  25209  mpomulcn  25221  fsumcn  25224  elcncf2  25244  cncfmet  25263  pcoass  25378  lmcau  25667  rrxdstprj1  25763  pmltpc  25804  ivthlem2  25806  ivthlem3  25807  ovollb2  25843  volsup  25910  ioombl1  25916  ioorf  25927  dyadss  25948  dyaddisjlem  25949  dyadmax  25952  volcn  25960  cncombf  26012  mbflimsup  26020  itg2const2  26095  iblss2  26159  cpnord  26288  dvmptfsum  26328  fta1g  26521  plydivex  26651  fta1  26662  aannenlem1  26688  ulmdvlem3  26762  advlogexp  27016  cxpmul2z  27052  atantayl2  27299  jensen  27349  isppw2  27475  lgsqr  27711  lgsqrmodndvds  27713  lgsdchrval  27714  lgsquad3  27747  2sqb  27792  dchrisumlem3  27851  pntrsumbnd2  27927  noinfbnd1lem5  28117  noetasuplem4  28126  noetainflem4  28130  noetalem1  28131  conway  28198  eqcuts3  28223  madebdayim  28307  madebdaylemlrcut  28318  negsprop  28454  mulscom  28558  absmuls  28663  bdayons  28695  addonbday  28698  bdayfinbndlem1  28886  remulscl  28921  tgjustf  28968  axsegcon  29538  axeuclidlem  29573  axcontlem9  29583  eengtrkg  29597  cusgrsize2inds  30067  pthdepisspth  30354  usgr2wlkneq  30375  crctcshwlkn0  30443  wpthswwlks2on  30586  clwwlkccatlem  30613  wwlksext2clwwlk  30681  umgr3v3e3cycl  30818  vdgn1frgrv2  30930  frgrwopreglem5  30955  frgrwopreg  30957  frgrhash2wsp  30966  numclwwlk1lem2fo  30992  vacn  31329  smcnlem  31332  0lno  31425  chocunii  31936  occl  31939  5oalem1  32289  3oalem2  32298  unoplin  32555  hmoplin  32577  lnconi  32668  kbass5  32755  mdslmd1lem1  32960  mdslmd1lem2  32961  mdsymlem2  33039  cdj1i  33068  cgrahlb  33080  opreu2reuALT  33148  unidifsnne  33207  disjabrex  33251  disjabrexf  33252  acunirnmpt  33328  fgreu  33340  suppovss  33348  xrge0infss  33425  xrofsup  33432  fsumiunle  33493  mgcf1o  33640  xrge0addgt0  33654  fzto1st1  33739  cyc3genpm  33789  cycpmgcl  33790  submarchi  33823  archiabllem1  33830  archiabllem2a  33831  isarchiofld  33836  rlocval  33896  imaslmod  33998  lindfpropd  34021  unitprodclb  34028  drnglring  34108  dflring3  34113  dfufd2lem  34165  mplmulmvr  34254  lvecdim0  34322  constrmon  34459  constrextdg2  34464  locfinreflem  34555  zarcmplem  34596  rge0scvg  34664  lmxrge0  34667  lmdvg  34668  qqhval2  34697  esumrnmpt2  34783  esumfsup  34785  esumpcvgval  34793  esumcvg  34801  esumgect  34805  esumiun  34809  sigaclfu2  34836  sigainb  34852  insiga  34853  fiunelros  34890  measinblem  34936  measinb  34937  measdivcst  34940  measdivcstALTV  34941  omssubadd  35015  oddpwdc  35069  dstrvprob  35187  signsply0  35263  signstfvneq0  35284  bnj1408  35749  j0ltalephlem  36020  dfk12  36025  dfk22  36026  dfk32  36027  ptpconn  36178  sconnpi1  36184  resconn  36191  cvmliftmolem2  36227  cvmlift2lem12  36259  satfsschain  36309  satffunlem2lem1  36349  ifscgr  37000  cgrxfr  37011  outsideofeu  37087  linethru  37109  nmulcom  37134  nmuladdss  37153  neibastop1  37338  dnicn  37549  irrdifflemf  38451  irrdiff  38452  fin2so  38735  poimirlem28  38771  poimirlem31  38774  mblfinlem2  38781  mblfinlem3  38782  itg2addnclem  38794  ftc1anclem7  38822  ftc1anclem8  38823  ftc1anc  38824  ssbnd  38925  totbndbnd  38926  prtlem10  40125  lssats  40272  lkrlss  40355  lshpset2N  40379  2dim  40730  islvol5  40839  paddasslem11  41090  pexmidlem8N  41237  ltrnid  41395  idltrn  41410  trlator0  41431  trlnidatb  41437  cdlemf2  41822  cdlemg2cex  41851  tendodi1  42044  tendodi2  42045  diblss  42430  dihopelvalcpre  42508  dih1dimatlem  42589  dihglblem6  42600  primrootscoprmpow  43352  posbezout  43353  aks6d1c4  43377  sticksstones22  43421  aks6d1c6isolem1  43427  aks6d1c6isolem2  43428  aks6d1c6lem5  43430  grpods  43447  unitscyglem3  43450  unitscyglem4  43451  remul01  43662  sn-subeu  43682  sn-0tie0  43719  prjspertr  43837  prjspersym  43839  0prjspnrel  43867  mzpsubst  43963  mzpcompact2lem  43966  eldioph2  43977  eldioph2b  43978  diophren  44024  pell14qrexpcl  44078  elpell1qr2  44083  monotoddzzfi  44153  acongtr  44189  acongrep  44191  jm2.19lem4  44203  jm2.26a  44211  jm2.26lem3  44212  jm2.26  44213  isnumbasgrplem2  44309  mendassa  44395  omord2lim  44505  cantnftermord  44525  tfsconcatfv1  44544  tfsconcatfv2  44545  naddcnffo  44569  naddcnfcom  44571  naddcnfid1  44572  naddgeoa  44599  clsk3nimkb  45243  prmunb2  45498  4an4132  45684  fiiuncl  46298  ssinc  46317  ssdec  46318  supxrgelem  46564  infxr  46593  cvgcaule  46716  mullimc  46843  mullimcf  46850  neglimc  46872  climleltrp  46901  climisp  46971  limsupresxr  46991  liminfresxr  46992  liminflimsupclim  47032  xlimliminflimsup  47087  icccncfext  47112  cncfiooicclem1  47118  fprodcncf  47125  dvnprodlem3  47173  iblcncfioo  47203  itgspltprt  47204  stoweidlem7  47232  stoweidlem28  47253  stoweidlem34  47259  stoweidlem48  47273  stoweidlem52  47277  wallispilem3  47292  fourierdlem12  47344  fourierdlem38  47370  fourierdlem39  47371  fourierdlem42  47374  fourierdlem46  47377  fourierdlem48  47379  fourierdlem49  47380  fourierdlem50  47381  fourierdlem51  47382  fourierdlem65  47396  fourierdlem73  47404  fourierdlem76  47407  fourierdlem87  47418  fourierdlem103  47434  fourierdlem104  47435  sge0f1o  47607  sge0le  47632  sge0reuz  47672  ismeannd  47692  isomenndlem  47755  hoicvr  47773  hoidmvle  47825  smflimlem2  47997  smflimmpt  48035  fsupdm  48067  finfdm  48071  nndivides2  48669  imasetpreimafvbijlemf1  48701  nnsum4primeseven  49113  nnsum4primesevenALTV  49114  bgoldbtbndlem2  49119  bgoldbtbndlem3  49120  bgoldbtbnd  49122  isubgr3stgrlem6  49284  rrxlinec  50064  iccdisj  50227  upfval  50507  fullthinc  50800  tanhadd  51142