Theorem simplll 774

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  7242  poseq  8140  oeeui  8569  oaabs2  8616  naddssim  8652  omxpenlem  9047  findcard3  9236  wemappo  9509  acndom2  10014  infpwfien  10022  sornom  10237  isf32lem2  10314  isf32lem4  10316  fin1a2lem11  10370  pwfseq  10624  gchina  10659  inttsk  10734  inar1  10735  prlem936  11007  mulcmpblnr  11031  00id  11356  mul02lem1  11357  addrid  11361  cnegex  11362  negeu  11418  add20  11697  ltmul12a  12045  lediv12a  12083  cru  12185  qextltlem  13169  xmullem  13231  xlemul1a  13255  ixxss12  13333  ioodisj  13450  elfz0fzfz0  13601  fsuppmapnn0fz  13968  seqf1o  14015  mulexpz  14074  leexp1a  14147  seqcoll  14436  swrdswrdlem  14676  pfxccatin12lem3  14704  abs3lem  15312  cau3lem  15328  climcau  15644  sumeq2ii  15666  climcndslem1  15822  climcndslem2  15823  geomulcvg  15849  mertenslem1  15857  mertenslem2  15858  mertens  15859  prodeq2ii  15884  prodmolem2  15908  bitsfzo  16412  sadadd2lem2  16427  dvdsmulgcd  16533  qredeu  16635  pc2dvds  16857  pcz  16859  ramcl  17007  firest  17402  mreexexlemd  17612  isacs2  17621  iscatd2  17649  ipodrsima  18507  mrelatlub  18528  mgmhmeql  18650  sgrppropd  18665  mndpropd  18693  mhmeql  18760  mhmid  19002  mhmmnd  19003  issubg4  19084  cycsubm  19141  cycsubmcom  19143  gasubg  19241  symgextf  19354  pmtr3ncom  19412  gexdvds  19521  oddvdssubg  19792  imasabl  19813  cyggeninv  19820  cyggenod  19821  issrg  20104  dvdsrmul1  20285  unitgrp  20299  cntzsubrng  20483  cntzsubr  20522  islmhm2  20952  lmhmeql  20969  lbspropd  21013  lssacsex  21061  rngqiprngimfo  21218  psgndiflemA  21517  isphl  21544  ocvocv  21587  lindfmm  21743  issubassa2  21808  mplbas2  21956  scmatmats  22405  smatvscl  22418  mdetdiag  22493  m2cpmfo  22650  pmatcollpw3fi1lem1  22680  pm2mpf1  22693  pm2mpghm  22710  fvmptnn04if  22743  chfacfscmulfsupp  22753  chfacfpmmulfsupp  22757  neissex  23021  neiptoptop  23025  neiptopnei  23026  restbas  23052  tgrest  23053  restopnb  23069  cnpco  23161  isreg2  23271  iunconn  23322  1stcrest  23347  2ndcctbss  23349  2ndcomap  23352  2ndcsep  23353  dislly  23391  kgencn2  23451  ptbasfi  23475  txhaus  23541  txkgen  23546  txconn  23583  qtopcn  23608  regr1lem2  23634  kqnrmlem1  23637  kqnrmlem2  23638  trfbas2  23737  trfil2  23781  flimcf  23876  hauspwpwf1  23881  fclscf  23919  flimfnfcls  23922  ustexsym  24110  ustuqtop4  24139  utop3cls  24146  utopreg  24147  ucnima  24175  ucncn  24179  metequiv2  24405  prdsxmslem2  24424  metcnpi3  24441  metustto  24448  metustid  24449  metustexhalf  24451  ngptgp  24531  xrsblre  24707  icccmp  24721  reconnlem1  24722  reconn  24724  opnreen  24727  metdsf  24744  metdscn  24752  mpomulcn  24765  fsumcn  24768  elcncf2  24790  cncfmet  24809  pcoass  24931  lmcau  25220  rrxdstprj1  25316  pmltpc  25358  ivthlem2  25360  ivthlem3  25361  ovollb2  25397  volsup  25464  ioombl1  25470  ioorf  25481  dyadss  25502  dyaddisjlem  25503  dyadmax  25506  volcn  25514  cncombf  25566  mbflimsup  25574  itg2const2  25649  iblss2  25714  cpnord  25844  dvmptfsum  25886  fta1g  26082  plydivex  26212  fta1  26223  aannenlem1  26243  ulmdvlem3  26318  advlogexp  26571  cxpmul2z  26607  atantayl2  26855  jensen  26906  isppw2  27032  lgsqr  27269  lgsqrmodndvds  27271  lgsdchrval  27272  lgsquad3  27305  2sqb  27350  dchrisumlem3  27409  pntrsumbnd2  27485  noinfbnd1lem5  27646  noetasuplem4  27655  noetainflem4  27659  noetalem1  27660  conway  27718  madebdayim  27806  madebdaylemlrcut  27817  negsprop  27948  mulscom  28049  absmuls  28153  bdayon  28180  remulscl  28360  tgjustf  28407  axsegcon  28861  axeuclidlem  28896  axcontlem9  28906  eengtrkg  28920  cusgrsize2inds  29388  pthdepisspth  29672  usgr2wlkneq  29693  crctcshwlkn0  29758  wpthswwlks2on  29898  clwwlkccatlem  29925  wwlksext2clwwlk  29993  umgr3v3e3cycl  30120  vdgn1frgrv2  30232  frgrwopreglem5  30257  frgrwopreg  30259  frgrhash2wsp  30268  numclwwlk1lem2fo  30294  vacn  30630  smcnlem  30633  0lno  30726  chocunii  31237  occl  31240  5oalem1  31590  3oalem2  31599  unoplin  31856  hmoplin  31878  lnconi  31969  kbass5  32056  mdslmd1lem1  32261  mdslmd1lem2  32262  mdsymlem2  32340  cdj1i  32369  opreu2reuALT  32413  unidifsnne  32472  disjabrex  32518  disjabrexf  32519  acunirnmpt  32590  fgreu  32603  suppovss  32611  xrge0infss  32690  xrofsup  32697  fsumiunle  32761  sgnmul  32767  sgnsub  32769  mgcf1o  32936  xrge0addgt0  32965  submomnd  33031  fzto1st1  33066  cyc3genpm  33116  cycpmgcl  33117  submarchi  33147  archiabllem1  33154  archiabllem2a  33155  rlocval  33217  isarchiofld  33302  imaslmod  33331  lindfpropd  33360  unitprodclb  33367  elrspunidl  33406  dfufd2lem  33527  lvecdim0  33609  constrmon  33741  constrextdg2  33746  locfinreflem  33837  zarcmplem  33878  rge0scvg  33946  lmxrge0  33949  lmdvg  33950  qqhval2  33979  esumrnmpt2  34065  esumfsup  34067  esumpcvgval  34075  esumcvg  34083  esumgect  34087  esumiun  34091  sigaclfu2  34118  sigainb  34133  insiga  34134  fiunelros  34171  measinblem  34217  measinb  34218  measdivcst  34221  measdivcstALTV  34222  omssubadd  34298  oddpwdc  34352  dstrvprob  34470  signsply0  34549  signstfvneq0  34570  bnj1408  35033  ptpconn  35227  sconnpi1  35233  resconn  35240  cvmliftmolem2  35276  cvmlift2lem12  35308  satfsschain  35358  satffunlem2lem1  35398  ifscgr  36039  cgrxfr  36050  outsideofeu  36126  linethru  36148  neibastop1  36354  dnicn  36487  irrdifflemf  37320  irrdiff  37321  fin2so  37608  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem28  37649  poimirlem31  37652  mblfinlem2  37659  mblfinlem3  37660  itg2addnclem  37672  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  ssbnd  37789  totbndbnd  37790  prtlem10  38865  lssats  39012  lkrlss  39095  lshpset2N  39119  2dim  39471  islvol5  39580  paddasslem11  39831  pexmidlem8N  39978  ltrnid  40136  idltrn  40151  trlator0  40172  trlnidatb  40178  cdlemf2  40563  cdlemg2cex  40592  tendodi1  40785  tendodi2  40786  diblss  41171  dihopelvalcpre  41249  dih1dimatlem  41330  dihglblem6  41341  primrootscoprmpow  42094  posbezout  42095  aks6d1c4  42119  sticksstones22  42163  aks6d1c6isolem1  42169  aks6d1c6isolem2  42170  aks6d1c6lem5  42172  grpods  42189  unitscyglem3  42192  unitscyglem4  42193  remul01  42402  sn-subeu  42422  sn-0tie0  42446  prjspertr  42600  prjspersym  42602  0prjspnrel  42622  mzpsubst  42743  mzpcompact2lem  42746  eldioph2  42757  eldioph2b  42758  diophren  42808  pell14qrexpcl  42862  elpell1qr2  42867  monotoddzzfi  42938  acongtr  42974  acongrep  42976  jm2.19lem4  42988  jm2.26a  42996  jm2.26lem3  42997  jm2.26  42998  isnumbasgrplem2  43100  mendassa  43186  omord2lim  43296  cantnftermord  43316  tfsconcatfv1  43335  tfsconcatfv2  43336  naddcnffo  43360  naddcnfcom  43362  naddcnfid1  43363  naddgeoa  43390  clsk3nimkb  44036  prmunb2  44307  4an4132  44496  fiiuncl  45066  ssinc  45088  ssdec  45089  supxrgelem  45340  infxr  45370  cvgcaule  45494  mullimc  45621  mullimcf  45628  neglimc  45652  climleltrp  45681  climisp  45751  limsupresxr  45771  liminfresxr  45772  liminflimsupclim  45812  xlimliminflimsup  45867  icccncfext  45892  cncfiooicclem1  45898  fprodcncf  45905  dvnprodlem3  45953  iblcncfioo  45983  itgspltprt  45984  stoweidlem7  46012  stoweidlem28  46033  stoweidlem34  46039  stoweidlem48  46053  stoweidlem52  46057  wallispilem3  46072  fourierdlem12  46124  fourierdlem38  46150  fourierdlem39  46151  fourierdlem42  46154  fourierdlem46  46157  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem51  46162  fourierdlem65  46176  fourierdlem73  46184  fourierdlem76  46187  fourierdlem87  46198  fourierdlem103  46214  fourierdlem104  46215  sge0f1o  46387  sge0le  46412  sge0reuz  46452  ismeannd  46472  isomenndlem  46535  hoicvr  46553  hoidmvle  46605  smflimlem2  46777  smflimmpt  46815  fsupdm  46847  finfdm  46851  imasetpreimafvbijlemf1  47409  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  bgoldbtbnd  47814  isubgr3stgrlem6  47974  rrxlinec  48729  iccdisj  48890  upfval  49169  fullthinc  49443