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  7264  poseq  8155  oeeui  8589  oaabs2  8636  naddssim  8673  omxpenlem  9067  findcard3  9244  wemappo  9512  acndom2  10039  infpwfien  10047  sornom  10262  isf32lem2  10339  isf32lem4  10341  fin1a2lem11  10395  pwfseq  10650  gchina  10685  inttsk  10760  inar1  10761  prlem936  11033  mulcmpblnr  11057  00id  11386  mul02lem1  11387  addrid  11391  cnegex  11392  negeu  11448  add20  11727  ltmul12a  12072  lediv12a  12109  cru  12211  qextltlem  13229  xmullem  13291  xlemul1a  13315  ixxss12  13393  ioodisj  13510  elfz0fzfz0  13663  fsuppmapnn0fz  14034  seqf1o  14081  mulexpz  14140  leexp1a  14213  seqcoll  14503  swrdswrdlem  14743  pfxccatin12lem3  14771  sgnsub  15145  sgnmul  15146  abs3lem  15392  cau3lem  15408  climcau  15724  sumeq2ii  15746  climcndslem1  15905  climcndslem2  15906  geomulcvg  15932  mertenslem1  15940  mertenslem2  15941  mertens  15942  prodeq2ii  15967  prodmolem2  15991  bitsfzo  16494  sadadd2lem2  16509  dvdsmulgcd  16615  qredeu  16717  pc2dvds  16940  pcz  16942  ramcl  17090  firest  17486  mreexexlemd  17701  isacs2  17710  iscatd2  17738  ipodrsima  18598  mrelatlub  18619  mgmhmeql  18775  sgrppropd  18790  mndpropd  18818  mhmeql  18886  mhmid  19130  mhmmnd  19131  issubg4  19213  cycsubm  19274  cycsubmcom  19276  gasubg  19373  symgextf  19488  pmtr3ncom  19546  gexdvds  19655  oddvdssubg  19926  imasabl  19947  cyggeninv  19954  cyggenod  19955  submomnd  20203  issrg  20271  dvdsrmul1  20452  unitgrp  20466  cntzsubrng  20653  cntzsubr  20692  islmhm2  21140  lmhmeql  21157  lbspropd  21201  lssacsex  21249  rngqiprngimfo  21422  psgndiflemA  21732  isphl  21759  ocvocv  21802  lindfmm  21958  issubassa2  22023  mplbas2  22174  scmatmats  22649  smatvscl  22662  mdetdiag  22737  m2cpmfo  22894  pmatcollpw3fi1lem1  22924  pm2mpf1  22937  pm2mpghm  22954  fvmptnn04if  22987  chfacfscmulfsupp  22997  chfacfpmmulfsupp  23001  neissex  23265  neiptoptop  23269  neiptopnei  23270  restbas  23296  tgrest  23297  restopnb  23313  cnpco  23405  isreg2  23515  iunconn  23566  1stcrest  23591  2ndcctbss  23593  2ndcomap  23596  2ndcsep  23597  dislly  23635  kgencn2  23695  ptbasfi  23719  txhaus  23785  txkgen  23790  txconn  23827  qtopcn  23852  regr1lem2  23878  kqnrmlem1  23881  kqnrmlem2  23882  trfbas2  23981  trfil2  24025  flimcf  24120  hauspwpwf1  24125  fclscf  24163  flimfnfcls  24166  ustexsym  24354  ustuqtop4  24382  utop3cls  24389  utopreg  24390  ucnima  24418  ucncn  24422  metequiv2  24648  prdsxmslem2  24667  metcnpi3  24684  metustto  24691  metustid  24692  metustexhalf  24694  ngptgp  24774  xrsblre  24950  icccmp  24964  reconnlem1  24965  reconn  24967  opnreen  24970  metdsf  24987  metdscn  24995  mpomulcn  25007  fsumcn  25010  elcncf2  25030  cncfmet  25049  pcoass  25164  lmcau  25453  rrxdstprj1  25549  pmltpc  25590  ivthlem2  25592  ivthlem3  25593  ovollb2  25629  volsup  25696  ioombl1  25702  ioorf  25713  dyadss  25734  dyaddisjlem  25735  dyadmax  25738  volcn  25746  cncombf  25798  mbflimsup  25806  itg2const2  25881  iblss2  25946  cpnord  26075  dvmptfsum  26115  fta1g  26308  plydivex  26439  fta1  26450  aannenlem1  26472  ulmdvlem3  26546  advlogexp  26801  cxpmul2z  26837  atantayl2  27084  jensen  27134  isppw2  27260  lgsqr  27496  lgsqrmodndvds  27498  lgsdchrval  27499  lgsquad3  27532  2sqb  27577  dchrisumlem3  27636  pntrsumbnd2  27712  noinfbnd1lem5  27872  noetasuplem4  27881  noetainflem4  27885  noetalem1  27886  conway  27953  eqcuts3  27978  madebdayim  28062  madebdaylemlrcut  28073  negsprop  28209  mulscom  28313  absmuls  28418  bdayons  28450  addonbday  28453  bdayfinbndlem1  28641  remulscl  28676  tgjustf  28723  axsegcon  29258  axeuclidlem  29293  axcontlem9  29303  eengtrkg  29317  cusgrsize2inds  29784  pthdepisspth  30065  usgr2wlkneq  30086  crctcshwlkn0  30151  wpthswwlks2on  30294  clwwlkccatlem  30321  wwlksext2clwwlk  30389  umgr3v3e3cycl  30516  vdgn1frgrv2  30628  frgrwopreglem5  30653  frgrwopreg  30655  frgrhash2wsp  30664  numclwwlk1lem2fo  30690  vacn  31027  smcnlem  31030  0lno  31123  chocunii  31634  occl  31637  5oalem1  31987  3oalem2  31996  unoplin  32253  hmoplin  32275  lnconi  32366  kbass5  32453  mdslmd1lem1  32658  mdslmd1lem2  32659  mdsymlem2  32737  cdj1i  32766  opreu2reuALT  32804  unidifsnne  32863  disjabrex  32908  disjabrexf  32909  acunirnmpt  32985  fgreu  32997  suppovss  33007  xrge0infss  33086  xrofsup  33093  fsumiunle  33154  mgcf1o  33304  xrge0addgt0  33318  fzto1st1  33403  cyc3genpm  33453  cycpmgcl  33454  submarchi  33487  archiabllem1  33494  archiabllem2a  33495  isarchiofld  33500  rlocval  33560  imaslmod  33654  lindfpropd  33676  unitprodclb  33683  elrspunidl  33717  drnglring  33763  dflring3  33768  dfufd2lem  33820  mplmulmvr  33910  lvecdim0  33978  constrmon  34115  constrextdg2  34120  locfinreflem  34211  zarcmplem  34252  rge0scvg  34320  lmxrge0  34323  lmdvg  34324  qqhval2  34353  esumrnmpt2  34439  esumfsup  34441  esumpcvgval  34449  esumcvg  34457  esumgect  34461  esumiun  34465  sigaclfu2  34492  sigainb  34507  insiga  34508  fiunelros  34545  measinblem  34591  measinb  34592  measdivcst  34595  measdivcstALTV  34596  omssubadd  34671  oddpwdc  34725  dstrvprob  34843  signsply0  34919  signstfvneq0  34940  bnj1408  35405  ptpconn  35706  sconnpi1  35712  resconn  35719  cvmliftmolem2  35755  cvmlift2lem12  35787  satfsschain  35837  satffunlem2lem1  35877  ifscgr  36517  cgrxfr  36528  outsideofeu  36604  linethru  36626  nmulcom  36667  nmuladdss  36671  neibastop1  36851  dnicn  37062  irrdifflemf  37950  irrdiff  37951  fin2so  38239  matunitlindflem1  38248  matunitlindflem2  38249  poimirlem28  38280  poimirlem31  38283  mblfinlem2  38290  mblfinlem3  38291  itg2addnclem  38303  ftc1anclem7  38331  ftc1anclem8  38332  ftc1anc  38333  ssbnd  38420  totbndbnd  38421  prtlem10  39620  lssats  39767  lkrlss  39850  lshpset2N  39874  2dim  40225  islvol5  40334  paddasslem11  40585  pexmidlem8N  40732  ltrnid  40890  idltrn  40905  trlator0  40926  trlnidatb  40932  cdlemf2  41317  cdlemg2cex  41346  tendodi1  41539  tendodi2  41540  diblss  41925  dihopelvalcpre  42003  dih1dimatlem  42084  dihglblem6  42095  primrootscoprmpow  42847  posbezout  42848  aks6d1c4  42872  sticksstones22  42916  aks6d1c6isolem1  42922  aks6d1c6isolem2  42923  aks6d1c6lem5  42925  grpods  42942  unitscyglem3  42945  unitscyglem4  42946  remul01  43149  sn-subeu  43169  sn-0tie0  43206  prjspertr  43320  prjspersym  43322  0prjspnrel  43342  mzpsubst  43462  mzpcompact2lem  43465  eldioph2  43476  eldioph2b  43477  diophren  43523  pell14qrexpcl  43577  elpell1qr2  43582  monotoddzzfi  43652  acongtr  43688  acongrep  43690  jm2.19lem4  43702  jm2.26a  43710  jm2.26lem3  43711  jm2.26  43712  isnumbasgrplem2  43814  mendassa  43900  omord2lim  44010  cantnftermord  44030  tfsconcatfv1  44049  tfsconcatfv2  44050  naddcnffo  44074  naddcnfcom  44076  naddcnfid1  44077  naddgeoa  44104  clsk3nimkb  44749  prmunb2  45004  4an4132  45191  fiiuncl  45768  ssinc  45788  ssdec  45789  supxrgelem  46036  infxr  46065  cvgcaule  46188  mullimc  46315  mullimcf  46322  neglimc  46344  climleltrp  46373  climisp  46443  limsupresxr  46463  liminfresxr  46464  liminflimsupclim  46504  xlimliminflimsup  46559  icccncfext  46584  cncfiooicclem1  46590  fprodcncf  46597  dvnprodlem3  46645  iblcncfioo  46675  itgspltprt  46676  stoweidlem7  46704  stoweidlem28  46725  stoweidlem34  46731  stoweidlem48  46745  stoweidlem52  46749  wallispilem3  46764  fourierdlem12  46816  fourierdlem38  46842  fourierdlem39  46843  fourierdlem42  46846  fourierdlem46  46849  fourierdlem48  46851  fourierdlem49  46852  fourierdlem50  46853  fourierdlem51  46854  fourierdlem65  46868  fourierdlem73  46876  fourierdlem76  46879  fourierdlem87  46890  fourierdlem103  46906  fourierdlem104  46907  sge0f1o  47079  sge0le  47104  sge0reuz  47144  ismeannd  47164  isomenndlem  47227  hoicvr  47245  hoidmvle  47297  smflimlem2  47469  smflimmpt  47507  fsupdm  47539  finfdm  47543  nndivides2  48104  imasetpreimafvbijlemf1  48136  nnsum4primeseven  48548  nnsum4primesevenALTV  48549  bgoldbtbndlem2  48554  bgoldbtbndlem3  48555  bgoldbtbnd  48557  isubgr3stgrlem6  48719  rrxlinec  49499  iccdisj  49659  upfval  49937  fullthinc  50211