Theorem simplll 773

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 22	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad3antrrr 728	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  f1imass  7271  poseq  8164  oeeui  8624  oaabs2  8671  naddssim  8707  omxpenlem  9103  findcard3  9312  wemappo  9585  acndom2  10090  infpwfien  10098  sornom  10311  isf32lem2  10388  isf32lem4  10390  fin1a2lem11  10444  pwfseq  10698  gchina  10733  inttsk  10808  inar1  10809  prlem936  11081  mulcmpblnr  11105  00id  11430  mul02lem1  11431  addrid  11435  cnegex  11436  negeu  11491  add20  11767  ltmul12a  12115  lediv12a  12153  cru  12250  qextltlem  13229  xmullem  13291  xlemul1a  13315  ixxss12  13392  ioodisj  13507  elfz0fzfz0  13654  fsuppmapnn0fz  14010  seqf1o  14057  mulexpz  14116  leexp1a  14188  seqcoll  14478  swrdswrdlem  14707  pfxccatin12lem3  14735  abs3lem  15338  cau3lem  15354  climcau  15670  sumeq2ii  15692  climcndslem1  15848  climcndslem2  15849  geomulcvg  15875  mertenslem1  15883  mertenslem2  15884  mertens  15885  prodeq2ii  15910  prodmolem2  15932  bitsfzo  16430  sadadd2lem2  16445  dvdsmulgcd  16552  qredeu  16654  pc2dvds  16876  pcz  16878  ramcl  17026  firest  17442  mreexexlemd  17652  isacs2  17661  iscatd2  17689  ipodrsima  18561  mrelatlub  18582  mgmhmeql  18704  sgrppropd  18719  mndpropd  18747  mhmeql  18811  mhmid  19053  mhmmnd  19054  issubg4  19135  cycsubm  19192  cycsubmcom  19194  gasubg  19292  symgextf  19411  pmtr3ncom  19469  gexdvds  19578  oddvdssubg  19849  imasabl  19870  cyggeninv  19877  cyggenod  19878  issrg  20167  dvdsrmul1  20347  unitgrp  20361  cntzsubrng  20545  cntzsubr  20586  islmhm2  21012  lmhmeql  21029  lbspropd  21073  lssacsex  21121  rngqiprngimfo  21286  psgndiflemA  21593  isphl  21620  ocvocv  21663  lindfmm  21821  issubassa2  21885  mplbas2  22045  scmatmats  22501  smatvscl  22514  mdetdiag  22589  m2cpmfo  22746  pmatcollpw3fi1lem1  22776  pm2mpf1  22789  pm2mpghm  22806  fvmptnn04if  22839  chfacfscmulfsupp  22849  chfacfpmmulfsupp  22853  neissex  23119  neiptoptop  23123  neiptopnei  23124  restbas  23150  tgrest  23151  restopnb  23167  cnpco  23259  isreg2  23369  iunconn  23420  1stcrest  23445  2ndcctbss  23447  2ndcomap  23450  2ndcsep  23451  dislly  23489  kgencn2  23549  ptbasfi  23573  txhaus  23639  txkgen  23644  txconn  23681  qtopcn  23706  regr1lem2  23732  kqnrmlem1  23735  kqnrmlem2  23736  trfbas2  23835  trfil2  23879  flimcf  23974  hauspwpwf1  23979  fclscf  24017  flimfnfcls  24020  ustexsym  24208  ustuqtop4  24237  utop3cls  24244  utopreg  24245  ucnima  24274  ucncn  24278  metequiv2  24507  prdsxmslem2  24526  metcnpi3  24543  metustto  24550  metustid  24551  metustexhalf  24553  ngptgp  24633  xrsblre  24815  icccmp  24829  reconnlem1  24830  reconn  24832  opnreen  24835  metdsf  24852  metdscn  24860  mpomulcn  24873  fsumcn  24876  elcncf2  24898  cncfmet  24917  pcoass  25039  lmcau  25329  rrxdstprj1  25425  pmltpc  25467  ivthlem2  25469  ivthlem3  25470  ovollb2  25506  volsup  25573  ioombl1  25579  ioorf  25590  dyadss  25611  dyaddisjlem  25612  dyadmax  25615  volcn  25623  cncombf  25675  mbflimsup  25683  itg2const2  25759  iblss2  25823  cpnord  25953  dvmptfsum  25995  fta1g  26194  plydivex  26322  fta1  26333  aannenlem1  26353  ulmdvlem3  26428  advlogexp  26679  cxpmul2z  26715  atantayl2  26963  jensen  27014  isppw2  27140  lgsqr  27377  lgsqrmodndvds  27379  lgsdchrval  27380  lgsquad3  27413  2sqb  27458  dchrisumlem3  27517  pntrsumbnd2  27593  noinfbnd1lem5  27754  noetasuplem4  27763  noetainflem4  27767  noetalem1  27768  conway  27826  madebdayim  27908  madebdaylemlrcut  27919  negsprop  28041  mulscom  28137  absmuls  28236  remulscl  28350  tgjustf  28397  axsegcon  28858  axeuclidlem  28893  axcontlem9  28903  eengtrkg  28917  cusgrsize2inds  29387  pthdepisspth  29669  usgr2wlkneq  29690  crctcshwlkn0  29752  wpthswwlks2on  29892  clwwlkccatlem  29919  wwlksext2clwwlk  29987  umgr3v3e3cycl  30114  vdgn1frgrv2  30226  frgrwopreglem5  30251  frgrwopreg  30253  frgrhash2wsp  30262  numclwwlk1lem2fo  30288  vacn  30624  smcnlem  30627  0lno  30720  chocunii  31231  occl  31234  5oalem1  31584  3oalem2  31593  unoplin  31850  hmoplin  31872  lnconi  31963  kbass5  32050  mdslmd1lem1  32255  mdslmd1lem2  32256  mdsymlem2  32334  cdj1i  32363  opreu2reuALT  32402  unidifsnne  32462  disjabrex  32502  disjabrexf  32503  acunirnmpt  32576  fgreu  32589  suppovss  32597  xrge0infss  32667  xrofsup  32674  fsumiunle  32733  mgcf1o  32876  xrge0addgt0  32903  submomnd  32949  fzto1st1  32984  cyc3genpm  33034  cycpmgcl  33035  submarchi  33055  archiabllem1  33062  archiabllem2a  33063  rlocval  33119  isarchiofld  33200  imaslmod  33234  lindfpropd  33263  unitprodclb  33270  elrspunidl  33309  dfufd2lem  33430  lvecdim0  33507  constrmon  33616  locfinreflem  33668  zarcmplem  33709  rge0scvg  33777  lmxrge0  33780  lmdvg  33781  qqhval2  33810  esumrnmpt2  33914  esumfsup  33916  esumpcvgval  33924  esumcvg  33932  esumgect  33936  esumiun  33940  sigaclfu2  33967  sigainb  33982  insiga  33983  fiunelros  34020  measinblem  34066  measinb  34067  measdivcst  34070  measdivcstALTV  34071  omssubadd  34147  oddpwdc  34201  dstrvprob  34318  sgnmul  34389  sgnsub  34391  signsply0  34410  signstfvneq0  34431  bnj1408  34894  ptpconn  35074  sconnpi1  35080  resconn  35087  cvmliftmolem2  35123  cvmlift2lem12  35155  satfsschain  35205  satffunlem2lem1  35245  ifscgr  35881  cgrxfr  35892  outsideofeu  35968  linethru  35990  neibastop1  36084  dnicn  36208  irrdifflemf  37045  irrdiff  37046  fin2so  37321  matunitlindflem1  37330  matunitlindflem2  37331  poimirlem28  37362  poimirlem31  37365  mblfinlem2  37372  mblfinlem3  37373  itg2addnclem  37385  ftc1anclem7  37413  ftc1anclem8  37414  ftc1anc  37415  ssbnd  37502  totbndbnd  37503  prtlem10  38576  lssats  38723  lkrlss  38806  lshpset2N  38830  2dim  39182  islvol5  39291  paddasslem11  39542  pexmidlem8N  39689  ltrnid  39847  idltrn  39862  trlator0  39883  trlnidatb  39889  cdlemf2  40274  cdlemg2cex  40303  tendodi1  40496  tendodi2  40497  diblss  40882  dihopelvalcpre  40960  dih1dimatlem  41041  dihglblem6  41052  primrootscoprmpow  41811  posbezout  41812  aks6d1c4  41836  sticksstones22  41880  aks6d1c6isolem1  41886  aks6d1c6isolem2  41887  aks6d1c6lem5  41889  grpods  41906  unitscyglem3  41909  unitscyglem4  41910  remul01  42118  sn-subeu  42137  sn-0tie0  42150  sn-itrere  42179  sn-retire  42180  prjspertr  42295  prjspersym  42297  0prjspnrel  42317  mzpsubst  42442  mzpcompact2lem  42445  eldioph2  42456  eldioph2b  42457  diophren  42507  pell14qrexpcl  42561  elpell1qr2  42566  monotoddzzfi  42637  acongtr  42673  acongrep  42675  jm2.19lem4  42687  jm2.26a  42695  jm2.26lem3  42696  jm2.26  42697  isnumbasgrplem2  42802  mendassa  42892  omord2lim  43003  cantnftermord  43023  tfsconcatfv1  43042  tfsconcatfv2  43043  naddcnffo  43067  naddcnfcom  43069  naddcnfid1  43070  naddgeoa  43098  clsk3nimkb  43744  prmunb2  44022  4an4132  44212  fiiuncl  44703  ssinc  44725  ssdec  44726  supxrgelem  44988  infxr  45018  cvgcaule  45143  mullimc  45273  mullimcf  45280  neglimc  45304  climleltrp  45333  climisp  45403  limsupresxr  45423  liminfresxr  45424  liminflimsupclim  45464  xlimliminflimsup  45519  icccncfext  45544  cncfiooicclem1  45550  fprodcncf  45557  dvnprodlem3  45605  iblcncfioo  45635  itgspltprt  45636  stoweidlem7  45664  stoweidlem28  45685  stoweidlem34  45691  stoweidlem48  45705  stoweidlem52  45709  wallispilem3  45724  fourierdlem12  45776  fourierdlem38  45802  fourierdlem39  45803  fourierdlem42  45806  fourierdlem46  45809  fourierdlem48  45811  fourierdlem49  45812  fourierdlem50  45813  fourierdlem51  45814  fourierdlem65  45828  fourierdlem73  45836  fourierdlem76  45839  fourierdlem87  45850  fourierdlem103  45866  fourierdlem104  45867  sge0f1o  46039  sge0le  46064  sge0reuz  46104  ismeannd  46124  isomenndlem  46187  hoicvr  46205  hoidmvle  46257  smflimlem2  46429  smflimmpt  46467  fsupdm  46499  finfdm  46503  imasetpreimafvbijlemf1  47012  nnsum4primeseven  47408  nnsum4primesevenALTV  47409  bgoldbtbndlem2  47414  bgoldbtbndlem3  47415  bgoldbtbnd  47417  rrxlinec  48160  iccdisj  48268  fullthinc  48403