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  7220  poseq  8110  oeeui  8540  oaabs2  8587  naddssim  8623  omxpenlem  9018  findcard3  9195  wemappo  9466  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  11320  mul02lem1  11321  addrid  11325  cnegex  11326  negeu  11382  add20  11661  ltmul12a  12009  lediv12a  12047  cru  12149  qextltlem  13129  xmullem  13191  xlemul1a  13215  ixxss12  13293  ioodisj  13410  elfz0fzfz0  13561  fsuppmapnn0fz  13931  seqf1o  13978  mulexpz  14037  leexp1a  14110  seqcoll  14399  swrdswrdlem  14639  pfxccatin12lem3  14667  abs3lem  15274  cau3lem  15290  climcau  15606  sumeq2ii  15628  climcndslem1  15784  climcndslem2  15785  geomulcvg  15811  mertenslem1  15819  mertenslem2  15820  mertens  15821  prodeq2ii  15846  prodmolem2  15870  bitsfzo  16374  sadadd2lem2  16389  dvdsmulgcd  16495  qredeu  16597  pc2dvds  16819  pcz  16821  ramcl  16969  firest  17364  mreexexlemd  17579  isacs2  17588  iscatd2  17616  ipodrsima  18476  mrelatlub  18497  mgmhmeql  18653  sgrppropd  18668  mndpropd  18696  mhmeql  18763  mhmid  19005  mhmmnd  19006  issubg4  19087  cycsubm  19143  cycsubmcom  19145  gasubg  19243  symgextf  19358  pmtr3ncom  19416  gexdvds  19525  oddvdssubg  19796  imasabl  19817  cyggeninv  19824  cyggenod  19825  submomnd  20073  issrg  20135  dvdsrmul1  20317  unitgrp  20331  cntzsubrng  20512  cntzsubr  20551  islmhm2  21002  lmhmeql  21019  lbspropd  21063  lssacsex  21111  rngqiprngimfo  21268  psgndiflemA  21568  isphl  21595  ocvocv  21638  lindfmm  21794  issubassa2  21860  mplbas2  22009  scmatmats  22467  smatvscl  22480  mdetdiag  22555  m2cpmfo  22712  pmatcollpw3fi1lem1  22742  pm2mpf1  22755  pm2mpghm  22772  fvmptnn04if  22805  chfacfscmulfsupp  22815  chfacfpmmulfsupp  22819  neissex  23083  neiptoptop  23087  neiptopnei  23088  restbas  23114  tgrest  23115  restopnb  23131  cnpco  23223  isreg2  23333  iunconn  23384  1stcrest  23409  2ndcctbss  23411  2ndcomap  23414  2ndcsep  23415  dislly  23453  kgencn2  23513  ptbasfi  23537  txhaus  23603  txkgen  23608  txconn  23645  qtopcn  23670  regr1lem2  23696  kqnrmlem1  23699  kqnrmlem2  23700  trfbas2  23799  trfil2  23843  flimcf  23938  hauspwpwf1  23943  fclscf  23981  flimfnfcls  23984  ustexsym  24172  ustuqtop4  24200  utop3cls  24207  utopreg  24208  ucnima  24236  ucncn  24240  metequiv2  24466  prdsxmslem2  24485  metcnpi3  24502  metustto  24509  metustid  24510  metustexhalf  24512  ngptgp  24592  xrsblre  24768  icccmp  24782  reconnlem1  24783  reconn  24785  opnreen  24788  metdsf  24805  metdscn  24813  mpomulcn  24826  fsumcn  24829  elcncf2  24851  cncfmet  24870  pcoass  24992  lmcau  25281  rrxdstprj1  25377  pmltpc  25419  ivthlem2  25421  ivthlem3  25422  ovollb2  25458  volsup  25525  ioombl1  25531  ioorf  25542  dyadss  25563  dyaddisjlem  25564  dyadmax  25567  volcn  25575  cncombf  25627  mbflimsup  25635  itg2const2  25710  iblss2  25775  cpnord  25905  dvmptfsum  25947  fta1g  26143  plydivex  26273  fta1  26284  aannenlem1  26304  ulmdvlem3  26379  advlogexp  26632  cxpmul2z  26668  atantayl2  26916  jensen  26967  isppw2  27093  lgsqr  27330  lgsqrmodndvds  27332  lgsdchrval  27333  lgsquad3  27366  2sqb  27411  dchrisumlem3  27470  pntrsumbnd2  27546  noinfbnd1lem5  27707  noetasuplem4  27716  noetainflem4  27720  noetalem1  27721  conway  27787  eqcuts3  27812  madebdayim  27896  madebdaylemlrcut  27907  negsprop  28043  mulscom  28147  absmuls  28252  bdayons  28284  addonbday  28287  bdayfinbndlem1  28475  remulscl  28510  tgjustf  28557  axsegcon  29012  axeuclidlem  29047  axcontlem9  29057  eengtrkg  29071  cusgrsize2inds  29539  pthdepisspth  29820  usgr2wlkneq  29841  crctcshwlkn0  29906  wpthswwlks2on  30049  clwwlkccatlem  30076  wwlksext2clwwlk  30144  umgr3v3e3cycl  30271  vdgn1frgrv2  30383  frgrwopreglem5  30408  frgrwopreg  30410  frgrhash2wsp  30419  numclwwlk1lem2fo  30445  vacn  30781  smcnlem  30784  0lno  30877  chocunii  31388  occl  31391  5oalem1  31741  3oalem2  31750  unoplin  32007  hmoplin  32029  lnconi  32120  kbass5  32207  mdslmd1lem1  32412  mdslmd1lem2  32413  mdsymlem2  32491  cdj1i  32520  opreu2reuALT  32562  unidifsnne  32622  disjabrex  32668  disjabrexf  32669  acunirnmpt  32748  fgreu  32760  suppovss  32770  xrge0infss  32850  xrofsup  32857  fsumiunle  32920  sgnmul  32926  sgnsub  32928  mgcf1o  33095  xrge0addgt0  33109  fzto1st1  33195  cyc3genpm  33245  cycpmgcl  33246  submarchi  33279  archiabllem1  33286  archiabllem2a  33287  isarchiofld  33292  rlocval  33352  imaslmod  33445  lindfpropd  33474  unitprodclb  33481  elrspunidl  33520  dfufd2lem  33641  mplmulmvr  33715  lvecdim0  33783  constrmon  33921  constrextdg2  33926  locfinreflem  34017  zarcmplem  34058  rge0scvg  34126  lmxrge0  34129  lmdvg  34130  qqhval2  34159  esumrnmpt2  34245  esumfsup  34247  esumpcvgval  34255  esumcvg  34263  esumgect  34267  esumiun  34271  sigaclfu2  34298  sigainb  34313  insiga  34314  fiunelros  34351  measinblem  34397  measinb  34398  measdivcst  34401  measdivcstALTV  34402  omssubadd  34477  oddpwdc  34531  dstrvprob  34649  signsply0  34728  signstfvneq0  34749  bnj1408  35211  ptpconn  35446  sconnpi1  35452  resconn  35459  cvmliftmolem2  35495  cvmlift2lem12  35527  satfsschain  35577  satffunlem2lem1  35617  ifscgr  36257  cgrxfr  36268  outsideofeu  36344  linethru  36366  neibastop1  36572  dnicn  36711  irrdifflemf  37577  irrdiff  37578  fin2so  37855  matunitlindflem1  37864  matunitlindflem2  37865  poimirlem28  37896  poimirlem31  37899  mblfinlem2  37906  mblfinlem3  37907  itg2addnclem  37919  ftc1anclem7  37947  ftc1anclem8  37948  ftc1anc  37949  ssbnd  38036  totbndbnd  38037  prtlem10  39238  lssats  39385  lkrlss  39468  lshpset2N  39492  2dim  39843  islvol5  39952  paddasslem11  40203  pexmidlem8N  40350  ltrnid  40508  idltrn  40523  trlator0  40544  trlnidatb  40550  cdlemf2  40935  cdlemg2cex  40964  tendodi1  41157  tendodi2  41158  diblss  41543  dihopelvalcpre  41621  dih1dimatlem  41702  dihglblem6  41713  primrootscoprmpow  42466  posbezout  42467  aks6d1c4  42491  sticksstones22  42535  aks6d1c6isolem1  42541  aks6d1c6isolem2  42542  aks6d1c6lem5  42544  grpods  42561  unitscyglem3  42564  unitscyglem4  42565  remul01  42774  sn-subeu  42794  sn-0tie0  42818  prjspertr  42960  prjspersym  42962  0prjspnrel  42982  mzpsubst  43102  mzpcompact2lem  43105  eldioph2  43116  eldioph2b  43117  diophren  43167  pell14qrexpcl  43221  elpell1qr2  43226  monotoddzzfi  43296  acongtr  43332  acongrep  43334  jm2.19lem4  43346  jm2.26a  43354  jm2.26lem3  43355  jm2.26  43356  isnumbasgrplem2  43458  mendassa  43544  omord2lim  43654  cantnftermord  43674  tfsconcatfv1  43693  tfsconcatfv2  43694  naddcnffo  43718  naddcnfcom  43720  naddcnfid1  43721  naddgeoa  43748  clsk3nimkb  44393  prmunb2  44664  4an4132  44852  fiiuncl  45422  ssinc  45443  ssdec  45444  supxrgelem  45693  infxr  45722  cvgcaule  45846  mullimc  45973  mullimcf  45980  neglimc  46002  climleltrp  46031  climisp  46101  limsupresxr  46121  liminfresxr  46122  liminflimsupclim  46162  xlimliminflimsup  46217  icccncfext  46242  cncfiooicclem1  46248  fprodcncf  46255  dvnprodlem3  46303  iblcncfioo  46333  itgspltprt  46334  stoweidlem7  46362  stoweidlem28  46383  stoweidlem34  46389  stoweidlem48  46403  stoweidlem52  46407  wallispilem3  46422  fourierdlem12  46474  fourierdlem38  46500  fourierdlem39  46501  fourierdlem42  46504  fourierdlem46  46507  fourierdlem48  46509  fourierdlem49  46510  fourierdlem50  46511  fourierdlem51  46512  fourierdlem65  46526  fourierdlem73  46534  fourierdlem76  46537  fourierdlem87  46548  fourierdlem103  46564  fourierdlem104  46565  sge0f1o  46737  sge0le  46762  sge0reuz  46802  ismeannd  46822  isomenndlem  46885  hoicvr  46903  hoidmvle  46955  smflimlem2  47127  smflimmpt  47165  fsupdm  47197  finfdm  47201  imasetpreimafvbijlemf1  47761  nnsum4primeseven  48157  nnsum4primesevenALTV  48158  bgoldbtbndlem2  48163  bgoldbtbndlem3  48164  bgoldbtbnd  48166  isubgr3stgrlem6  48328  rrxlinec  49093  iccdisj  49254  upfval  49532  fullthinc  49806