Theorem simplll 775

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  f1imass  7284  poseq  8183  oeeui  8640  oaabs2  8687  naddssim  8723  omxpenlem  9113  findcard3  9318  wemappo  9589  acndom2  10094  infpwfien  10102  sornom  10317  isf32lem2  10394  isf32lem4  10396  fin1a2lem11  10450  pwfseq  10704  gchina  10739  inttsk  10814  inar1  10815  prlem936  11087  mulcmpblnr  11111  00id  11436  mul02lem1  11437  addrid  11441  cnegex  11442  negeu  11498  add20  11775  ltmul12a  12123  lediv12a  12161  cru  12258  qextltlem  13244  xmullem  13306  xlemul1a  13330  ixxss12  13407  ioodisj  13522  elfz0fzfz0  13673  fsuppmapnn0fz  14037  seqf1o  14084  mulexpz  14143  leexp1a  14215  seqcoll  14503  swrdswrdlem  14742  pfxccatin12lem3  14770  abs3lem  15377  cau3lem  15393  climcau  15707  sumeq2ii  15729  climcndslem1  15885  climcndslem2  15886  geomulcvg  15912  mertenslem1  15920  mertenslem2  15921  mertens  15922  prodeq2ii  15947  prodmolem2  15971  bitsfzo  16472  sadadd2lem2  16487  dvdsmulgcd  16593  qredeu  16695  pc2dvds  16917  pcz  16919  ramcl  17067  firest  17477  mreexexlemd  17687  isacs2  17696  iscatd2  17724  ipodrsima  18586  mrelatlub  18607  mgmhmeql  18729  sgrppropd  18744  mndpropd  18772  mhmeql  18839  mhmid  19081  mhmmnd  19082  issubg4  19163  cycsubm  19220  cycsubmcom  19222  gasubg  19320  symgextf  19435  pmtr3ncom  19493  gexdvds  19602  oddvdssubg  19873  imasabl  19894  cyggeninv  19901  cyggenod  19902  issrg  20185  dvdsrmul1  20369  unitgrp  20383  cntzsubrng  20567  cntzsubr  20606  islmhm2  21037  lmhmeql  21054  lbspropd  21098  lssacsex  21146  rngqiprngimfo  21311  psgndiflemA  21619  isphl  21646  ocvocv  21689  lindfmm  21847  issubassa2  21912  mplbas2  22060  scmatmats  22517  smatvscl  22530  mdetdiag  22605  m2cpmfo  22762  pmatcollpw3fi1lem1  22792  pm2mpf1  22805  pm2mpghm  22822  fvmptnn04if  22855  chfacfscmulfsupp  22865  chfacfpmmulfsupp  22869  neissex  23135  neiptoptop  23139  neiptopnei  23140  restbas  23166  tgrest  23167  restopnb  23183  cnpco  23275  isreg2  23385  iunconn  23436  1stcrest  23461  2ndcctbss  23463  2ndcomap  23466  2ndcsep  23467  dislly  23505  kgencn2  23565  ptbasfi  23589  txhaus  23655  txkgen  23660  txconn  23697  qtopcn  23722  regr1lem2  23748  kqnrmlem1  23751  kqnrmlem2  23752  trfbas2  23851  trfil2  23895  flimcf  23990  hauspwpwf1  23995  fclscf  24033  flimfnfcls  24036  ustexsym  24224  ustuqtop4  24253  utop3cls  24260  utopreg  24261  ucnima  24290  ucncn  24294  metequiv2  24523  prdsxmslem2  24542  metcnpi3  24559  metustto  24566  metustid  24567  metustexhalf  24569  ngptgp  24649  xrsblre  24833  icccmp  24847  reconnlem1  24848  reconn  24850  opnreen  24853  metdsf  24870  metdscn  24878  mpomulcn  24891  fsumcn  24894  elcncf2  24916  cncfmet  24935  pcoass  25057  lmcau  25347  rrxdstprj1  25443  pmltpc  25485  ivthlem2  25487  ivthlem3  25488  ovollb2  25524  volsup  25591  ioombl1  25597  ioorf  25608  dyadss  25629  dyaddisjlem  25630  dyadmax  25633  volcn  25641  cncombf  25693  mbflimsup  25701  itg2const2  25776  iblss2  25841  cpnord  25971  dvmptfsum  26013  fta1g  26209  plydivex  26339  fta1  26350  aannenlem1  26370  ulmdvlem3  26445  advlogexp  26697  cxpmul2z  26733  atantayl2  26981  jensen  27032  isppw2  27158  lgsqr  27395  lgsqrmodndvds  27397  lgsdchrval  27398  lgsquad3  27431  2sqb  27476  dchrisumlem3  27535  pntrsumbnd2  27611  noinfbnd1lem5  27772  noetasuplem4  27781  noetainflem4  27785  noetalem1  27786  conway  27844  madebdayim  27926  madebdaylemlrcut  27937  negsprop  28067  mulscom  28165  absmuls  28268  remulscl  28434  tgjustf  28481  axsegcon  28942  axeuclidlem  28977  axcontlem9  28987  eengtrkg  29001  cusgrsize2inds  29471  pthdepisspth  29755  usgr2wlkneq  29776  crctcshwlkn0  29841  wpthswwlks2on  29981  clwwlkccatlem  30008  wwlksext2clwwlk  30076  umgr3v3e3cycl  30203  vdgn1frgrv2  30315  frgrwopreglem5  30340  frgrwopreg  30342  frgrhash2wsp  30351  numclwwlk1lem2fo  30377  vacn  30713  smcnlem  30716  0lno  30809  chocunii  31320  occl  31323  5oalem1  31673  3oalem2  31682  unoplin  31939  hmoplin  31961  lnconi  32052  kbass5  32139  mdslmd1lem1  32344  mdslmd1lem2  32345  mdsymlem2  32423  cdj1i  32452  opreu2reuALT  32496  unidifsnne  32554  disjabrex  32595  disjabrexf  32596  acunirnmpt  32669  fgreu  32682  suppovss  32690  xrge0infss  32764  xrofsup  32771  fsumiunle  32831  mgcf1o  32993  xrge0addgt0  33022  submomnd  33087  fzto1st1  33122  cyc3genpm  33172  cycpmgcl  33173  submarchi  33193  archiabllem1  33200  archiabllem2a  33201  rlocval  33263  isarchiofld  33347  imaslmod  33381  lindfpropd  33410  unitprodclb  33417  elrspunidl  33456  dfufd2lem  33577  lvecdim0  33657  constrmon  33785  constrextdg2  33790  locfinreflem  33839  zarcmplem  33880  rge0scvg  33948  lmxrge0  33951  lmdvg  33952  qqhval2  33983  esumrnmpt2  34069  esumfsup  34071  esumpcvgval  34079  esumcvg  34087  esumgect  34091  esumiun  34095  sigaclfu2  34122  sigainb  34137  insiga  34138  fiunelros  34175  measinblem  34221  measinb  34222  measdivcst  34225  measdivcstALTV  34226  omssubadd  34302  oddpwdc  34356  dstrvprob  34474  sgnmul  34545  sgnsub  34547  signsply0  34566  signstfvneq0  34587  bnj1408  35050  ptpconn  35238  sconnpi1  35244  resconn  35251  cvmliftmolem2  35287  cvmlift2lem12  35319  satfsschain  35369  satffunlem2lem1  35409  ifscgr  36045  cgrxfr  36056  outsideofeu  36132  linethru  36154  neibastop1  36360  dnicn  36493  irrdifflemf  37326  irrdiff  37327  fin2so  37614  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem28  37655  poimirlem31  37658  mblfinlem2  37665  mblfinlem3  37666  itg2addnclem  37678  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  ssbnd  37795  totbndbnd  37796  prtlem10  38866  lssats  39013  lkrlss  39096  lshpset2N  39120  2dim  39472  islvol5  39581  paddasslem11  39832  pexmidlem8N  39979  ltrnid  40137  idltrn  40152  trlator0  40173  trlnidatb  40179  cdlemf2  40564  cdlemg2cex  40593  tendodi1  40786  tendodi2  40787  diblss  41172  dihopelvalcpre  41250  dih1dimatlem  41331  dihglblem6  41342  primrootscoprmpow  42100  posbezout  42101  aks6d1c4  42125  sticksstones22  42169  aks6d1c6isolem1  42175  aks6d1c6isolem2  42176  aks6d1c6lem5  42178  grpods  42195  unitscyglem3  42198  unitscyglem4  42199  remul01  42437  sn-subeu  42456  sn-0tie0  42469  sn-itrere  42498  sn-retire  42499  prjspertr  42615  prjspersym  42617  0prjspnrel  42637  mzpsubst  42759  mzpcompact2lem  42762  eldioph2  42773  eldioph2b  42774  diophren  42824  pell14qrexpcl  42878  elpell1qr2  42883  monotoddzzfi  42954  acongtr  42990  acongrep  42992  jm2.19lem4  43004  jm2.26a  43012  jm2.26lem3  43013  jm2.26  43014  isnumbasgrplem2  43116  mendassa  43202  omord2lim  43313  cantnftermord  43333  tfsconcatfv1  43352  tfsconcatfv2  43353  naddcnffo  43377  naddcnfcom  43379  naddcnfid1  43380  naddgeoa  43407  clsk3nimkb  44053  prmunb2  44330  4an4132  44519  fiiuncl  45070  ssinc  45092  ssdec  45093  supxrgelem  45348  infxr  45378  cvgcaule  45502  mullimc  45631  mullimcf  45638  neglimc  45662  climleltrp  45691  climisp  45761  limsupresxr  45781  liminfresxr  45782  liminflimsupclim  45822  xlimliminflimsup  45877  icccncfext  45902  cncfiooicclem1  45908  fprodcncf  45915  dvnprodlem3  45963  iblcncfioo  45993  itgspltprt  45994  stoweidlem7  46022  stoweidlem28  46043  stoweidlem34  46049  stoweidlem48  46063  stoweidlem52  46067  wallispilem3  46082  fourierdlem12  46134  fourierdlem38  46160  fourierdlem39  46161  fourierdlem42  46164  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem51  46172  fourierdlem65  46186  fourierdlem73  46194  fourierdlem76  46197  fourierdlem87  46208  fourierdlem103  46224  fourierdlem104  46225  sge0f1o  46397  sge0le  46422  sge0reuz  46462  ismeannd  46482  isomenndlem  46545  hoicvr  46563  hoidmvle  46615  smflimlem2  46787  smflimmpt  46825  fsupdm  46857  finfdm  46861  imasetpreimafvbijlemf1  47391  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  bgoldbtbnd  47796  isubgr3stgrlem6  47938  rrxlinec  48657  iccdisj  48796  upfval  48933  fullthinc  49099