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 731	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  7219  poseq  8108  oeeui  8538  oaabs2  8585  naddssim  8621  omxpenlem  9016  findcard3  9193  wemappo  9464  acndom2  9976  infpwfien  9984  sornom  10199  isf32lem2  10276  isf32lem4  10278  fin1a2lem11  10332  pwfseq  10587  gchina  10622  inttsk  10697  inar1  10698  prlem936  10970  mulcmpblnr  10994  00id  11321  mul02lem1  11322  addrid  11326  cnegex  11327  negeu  11383  add20  11662  ltmul12a  12011  lediv12a  12049  cru  12151  qextltlem  13154  xmullem  13216  xlemul1a  13240  ixxss12  13318  ioodisj  13435  elfz0fzfz0  13587  fsuppmapnn0fz  13958  seqf1o  14005  mulexpz  14064  leexp1a  14137  seqcoll  14426  swrdswrdlem  14666  pfxccatin12lem3  14694  abs3lem  15301  cau3lem  15317  climcau  15633  sumeq2ii  15655  climcndslem1  15814  climcndslem2  15815  geomulcvg  15841  mertenslem1  15849  mertenslem2  15850  mertens  15851  prodeq2ii  15876  prodmolem2  15900  bitsfzo  16404  sadadd2lem2  16419  dvdsmulgcd  16525  qredeu  16627  pc2dvds  16850  pcz  16852  ramcl  17000  firest  17395  mreexexlemd  17610  isacs2  17619  iscatd2  17647  ipodrsima  18507  mrelatlub  18528  mgmhmeql  18684  sgrppropd  18699  mndpropd  18727  mhmeql  18794  mhmid  19039  mhmmnd  19040  issubg4  19121  cycsubm  19177  cycsubmcom  19179  gasubg  19277  symgextf  19392  pmtr3ncom  19450  gexdvds  19559  oddvdssubg  19830  imasabl  19851  cyggeninv  19858  cyggenod  19859  submomnd  20107  issrg  20169  dvdsrmul1  20349  unitgrp  20363  cntzsubrng  20544  cntzsubr  20583  islmhm2  21033  lmhmeql  21050  lbspropd  21094  lssacsex  21142  rngqiprngimfo  21299  psgndiflemA  21581  isphl  21608  ocvocv  21651  lindfmm  21807  issubassa2  21872  mplbas2  22020  scmatmats  22476  smatvscl  22489  mdetdiag  22564  m2cpmfo  22721  pmatcollpw3fi1lem1  22751  pm2mpf1  22764  pm2mpghm  22781  fvmptnn04if  22814  chfacfscmulfsupp  22824  chfacfpmmulfsupp  22828  neissex  23092  neiptoptop  23096  neiptopnei  23097  restbas  23123  tgrest  23124  restopnb  23140  cnpco  23232  isreg2  23342  iunconn  23393  1stcrest  23418  2ndcctbss  23420  2ndcomap  23423  2ndcsep  23424  dislly  23462  kgencn2  23522  ptbasfi  23546  txhaus  23612  txkgen  23617  txconn  23654  qtopcn  23679  regr1lem2  23705  kqnrmlem1  23708  kqnrmlem2  23709  trfbas2  23808  trfil2  23852  flimcf  23947  hauspwpwf1  23952  fclscf  23990  flimfnfcls  23993  ustexsym  24181  ustuqtop4  24209  utop3cls  24216  utopreg  24217  ucnima  24245  ucncn  24249  metequiv2  24475  prdsxmslem2  24494  metcnpi3  24511  metustto  24518  metustid  24519  metustexhalf  24521  ngptgp  24601  xrsblre  24777  icccmp  24791  reconnlem1  24792  reconn  24794  opnreen  24797  metdsf  24814  metdscn  24822  mpomulcn  24834  fsumcn  24837  elcncf2  24857  cncfmet  24876  pcoass  24991  lmcau  25280  rrxdstprj1  25376  pmltpc  25417  ivthlem2  25419  ivthlem3  25420  ovollb2  25456  volsup  25523  ioombl1  25529  ioorf  25540  dyadss  25561  dyaddisjlem  25562  dyadmax  25565  volcn  25573  cncombf  25625  mbflimsup  25633  itg2const2  25708  iblss2  25773  cpnord  25902  dvmptfsum  25942  fta1g  26135  plydivex  26263  fta1  26274  aannenlem1  26294  ulmdvlem3  26367  advlogexp  26619  cxpmul2z  26655  atantayl2  26902  jensen  26952  isppw2  27078  lgsqr  27314  lgsqrmodndvds  27316  lgsdchrval  27317  lgsquad3  27350  2sqb  27395  dchrisumlem3  27454  pntrsumbnd2  27530  noinfbnd1lem5  27691  noetasuplem4  27700  noetainflem4  27704  noetalem1  27705  conway  27771  eqcuts3  27796  madebdayim  27880  madebdaylemlrcut  27891  negsprop  28027  mulscom  28131  absmuls  28236  bdayons  28268  addonbday  28271  bdayfinbndlem1  28459  remulscl  28494  tgjustf  28541  axsegcon  28996  axeuclidlem  29031  axcontlem9  29041  eengtrkg  29055  cusgrsize2inds  29522  pthdepisspth  29803  usgr2wlkneq  29824  crctcshwlkn0  29889  wpthswwlks2on  30032  clwwlkccatlem  30059  wwlksext2clwwlk  30127  umgr3v3e3cycl  30254  vdgn1frgrv2  30366  frgrwopreglem5  30391  frgrwopreg  30393  frgrhash2wsp  30402  numclwwlk1lem2fo  30428  vacn  30765  smcnlem  30768  0lno  30861  chocunii  31372  occl  31375  5oalem1  31725  3oalem2  31734  unoplin  31991  hmoplin  32013  lnconi  32104  kbass5  32191  mdslmd1lem1  32396  mdslmd1lem2  32397  mdsymlem2  32475  cdj1i  32504  opreu2reuALT  32546  unidifsnne  32606  disjabrex  32652  disjabrexf  32653  acunirnmpt  32732  fgreu  32744  suppovss  32754  xrge0infss  32833  xrofsup  32840  fsumiunle  32902  sgnmul  32908  sgnsub  32910  mgcf1o  33063  xrge0addgt0  33077  fzto1st1  33163  cyc3genpm  33213  cycpmgcl  33214  submarchi  33247  archiabllem1  33254  archiabllem2a  33255  isarchiofld  33260  rlocval  33320  imaslmod  33413  lindfpropd  33442  unitprodclb  33449  elrspunidl  33488  dfufd2lem  33609  mplmulmvr  33683  lvecdim0  33751  constrmon  33888  constrextdg2  33893  locfinreflem  33984  zarcmplem  34025  rge0scvg  34093  lmxrge0  34096  lmdvg  34097  qqhval2  34126  esumrnmpt2  34212  esumfsup  34214  esumpcvgval  34222  esumcvg  34230  esumgect  34234  esumiun  34238  sigaclfu2  34265  sigainb  34280  insiga  34281  fiunelros  34318  measinblem  34364  measinb  34365  measdivcst  34368  measdivcstALTV  34369  omssubadd  34444  oddpwdc  34498  dstrvprob  34616  signsply0  34695  signstfvneq0  34716  bnj1408  35178  ptpconn  35415  sconnpi1  35421  resconn  35428  cvmliftmolem2  35464  cvmlift2lem12  35496  satfsschain  35546  satffunlem2lem1  35586  ifscgr  36226  cgrxfr  36237  outsideofeu  36313  linethru  36335  neibastop1  36541  dnicn  36752  irrdifflemf  37639  irrdiff  37640  fin2so  37928  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem28  37969  poimirlem31  37972  mblfinlem2  37979  mblfinlem3  37980  itg2addnclem  37992  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  ssbnd  38109  totbndbnd  38110  prtlem10  39311  lssats  39458  lkrlss  39541  lshpset2N  39565  2dim  39916  islvol5  40025  paddasslem11  40276  pexmidlem8N  40423  ltrnid  40581  idltrn  40596  trlator0  40617  trlnidatb  40623  cdlemf2  41008  cdlemg2cex  41037  tendodi1  41230  tendodi2  41231  diblss  41616  dihopelvalcpre  41694  dih1dimatlem  41775  dihglblem6  41786  primrootscoprmpow  42538  posbezout  42539  aks6d1c4  42563  sticksstones22  42607  aks6d1c6isolem1  42613  aks6d1c6isolem2  42614  aks6d1c6lem5  42616  grpods  42633  unitscyglem3  42636  unitscyglem4  42637  remul01  42839  sn-subeu  42859  sn-0tie0  42896  prjspertr  43038  prjspersym  43040  0prjspnrel  43060  mzpsubst  43180  mzpcompact2lem  43183  eldioph2  43194  eldioph2b  43195  diophren  43241  pell14qrexpcl  43295  elpell1qr2  43300  monotoddzzfi  43370  acongtr  43406  acongrep  43408  jm2.19lem4  43420  jm2.26a  43428  jm2.26lem3  43429  jm2.26  43430  isnumbasgrplem2  43532  mendassa  43618  omord2lim  43728  cantnftermord  43748  tfsconcatfv1  43767  tfsconcatfv2  43768  naddcnffo  43792  naddcnfcom  43794  naddcnfid1  43795  naddgeoa  43822  clsk3nimkb  44467  prmunb2  44738  4an4132  44926  fiiuncl  45496  ssinc  45517  ssdec  45518  supxrgelem  45767  infxr  45796  cvgcaule  45919  mullimc  46046  mullimcf  46053  neglimc  46075  climleltrp  46104  climisp  46174  limsupresxr  46194  liminfresxr  46195  liminflimsupclim  46235  xlimliminflimsup  46290  icccncfext  46315  cncfiooicclem1  46321  fprodcncf  46328  dvnprodlem3  46376  iblcncfioo  46406  itgspltprt  46407  stoweidlem7  46435  stoweidlem28  46456  stoweidlem34  46462  stoweidlem48  46476  stoweidlem52  46480  wallispilem3  46495  fourierdlem12  46547  fourierdlem38  46573  fourierdlem39  46574  fourierdlem42  46577  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem51  46585  fourierdlem65  46599  fourierdlem73  46607  fourierdlem76  46610  fourierdlem87  46621  fourierdlem103  46637  fourierdlem104  46638  sge0f1o  46810  sge0le  46835  sge0reuz  46875  ismeannd  46895  isomenndlem  46958  hoicvr  46976  hoidmvle  47028  smflimlem2  47200  smflimmpt  47238  fsupdm  47270  finfdm  47274  nndivides2  47832  imasetpreimafvbijlemf1  47864  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbnd  48285  isubgr3stgrlem6  48447  rrxlinec  49212  iccdisj  49373  upfval  49651  fullthinc  49925