Theorem simplll 787

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  f1imass  7268  poseq  8177  oeeui  8614  oaabs2  8661  naddssim  8698  omxpenlem  9100  findcard3  9277  wemappo  9546  acndom2  10136  infpwfien  10144  sornom  10358  isf32lem2  10435  isf32lem4  10437  fin1a2lem11  10491  pwfseq  10752  gchina  10787  inttsk  10862  inar1  10863  prlem936  11135  mulcmpblnr  11159  00id  11488  mul02lem1  11489  addrid  11493  cnegex  11494  negeu  11550  add20  11831  ltmul12a  12176  lediv12a  12213  cru  12315  qextltlem  13335  xmullem  13397  xlemul1a  13421  ixxss12  13499  ioodisj  13616  elfz0fzfz0  13770  fsuppmapnn0fz  14142  seqf1o  14189  mulexpz  14248  leexp1a  14321  seqcoll  14612  swrdswrdlem  14857  pfxccatin12lem3  14885  s3rex  15106  sgnsub  15264  sgnmul  15265  abs3lem  15511  cau3lem  15527  climcau  15843  sumeq2ii  15865  climcndslem1  16023  climcndslem2  16024  geomulcvg  16050  mertenslem1  16058  mertenslem2  16059  mertens  16060  prodeq2ii  16085  prodmolem2  16107  bitsfzo  16610  sadadd2lem2  16625  dvdsmulgcd  16735  qredeu  16838  pc2dvds  17062  pcz  17064  ramcl  17212  firest  17608  mreexexlemd  17823  isacs2  17832  iscatd2  17860  ipodrsima  18720  mrelatlub  18741  mgmhmeql  18910  sgrppropd  18925  mndpropd  18956  mhmeql  19027  mhmid  19278  mhmmnd  19279  issubg4  19361  cycsubm  19422  cycsubmcom  19424  gasubg  19521  symgextf  19636  pmtr3ncom  19694  gexdvds  19803  oddvdssubg  20074  imasabl  20095  cyggeninv  20102  cyggenod  20103  submomnd  20351  issrg  20419  dvdsrmul1  20604  unitgrp  20618  cntzsubrng  20824  cntzsubr  20863  islmhm2  21318  lmhmeql  21335  lbspropd  21379  lssacsex  21427  rngqiprngimfo  21602  psgndiflemA  21912  isphl  21939  ocvocv  21982  lindfmm  22138  issubassa2  22205  mplbas2  22356  scmatmats  22831  smatvscl  22844  mdetdiag  22919  matunitlindflem1  22999  matunitlindflem2  23000  m2cpmfo  23079  pmatcollpw3fi1lem1  23109  pm2mpf1  23122  pm2mpghm  23139  fvmptnn04if  23172  chfacfscmulfsupp  23182  chfacfpmmulfsupp  23186  neissex  23450  neiptoptop  23454  neiptopnei  23455  restbas  23481  tgrest  23482  restopnb  23498  cnpco  23590  isreg2  23700  iunconn  23751  1stcrest  23776  2ndcctbss  23779  2ndcomap  23782  2ndcsep  23783  dislly  23821  kgencn2  23881  ptbasfi  23905  txhaus  23971  txkgen  23976  txconn  24013  qtopcn  24038  regr1lem2  24064  kqnrmlem1  24067  kqnrmlem2  24068  trfbas2  24167  trfil2  24211  flimcf  24306  hauspwpwf1  24311  fclscf  24349  flimfnfcls  24352  ustexsym  24540  ustuqtop4  24568  utop3cls  24575  utopreg  24576  ucnima  24604  ucncn  24608  metequiv2  24834  prdsxmslem2  24853  metcnpi3  24870  metustto  24877  metustid  24878  metustexhalf  24880  ngptgp  24960  xrsblre  25136  icccmp  25150  reconnlem1  25151  reconn  25153  opnreen  25156  metdsf  25173  metdscn  25181  mpomulcn  25193  fsumcn  25196  elcncf2  25216  cncfmet  25235  pcoass  25350  lmcau  25639  rrxdstprj1  25735  pmltpc  25776  ivthlem2  25778  ivthlem3  25779  ovollb2  25815  volsup  25882  ioombl1  25888  ioorf  25899  dyadss  25920  dyaddisjlem  25921  dyadmax  25924  volcn  25932  cncombf  25984  mbflimsup  25992  itg2const2  26067  iblss2  26131  cpnord  26260  dvmptfsum  26300  fta1g  26493  plydivex  26623  fta1  26634  aannenlem1  26660  ulmdvlem3  26734  advlogexp  26988  cxpmul2z  27024  atantayl2  27271  jensen  27321  isppw2  27447  lgsqr  27683  lgsqrmodndvds  27685  lgsdchrval  27686  lgsquad3  27719  2sqb  27764  dchrisumlem3  27823  pntrsumbnd2  27899  noinfbnd1lem5  28089  noetasuplem4  28098  noetainflem4  28102  noetalem1  28103  conway  28170  eqcuts3  28195  madebdayim  28279  madebdaylemlrcut  28290  negsprop  28426  mulscom  28530  absmuls  28635  bdayons  28667  addonbday  28670  bdayfinbndlem1  28858  remulscl  28893  tgjustf  28940  axsegcon  29510  axeuclidlem  29545  axcontlem9  29555  eengtrkg  29569  cusgrsize2inds  30039  pthdepisspth  30326  usgr2wlkneq  30347  crctcshwlkn0  30415  wpthswwlks2on  30558  clwwlkccatlem  30585  wwlksext2clwwlk  30653  umgr3v3e3cycl  30790  vdgn1frgrv2  30902  frgrwopreglem5  30927  frgrwopreg  30929  frgrhash2wsp  30938  numclwwlk1lem2fo  30964  vacn  31301  smcnlem  31304  0lno  31397  chocunii  31908  occl  31911  5oalem1  32261  3oalem2  32270  unoplin  32527  hmoplin  32549  lnconi  32640  kbass5  32727  mdslmd1lem1  32932  mdslmd1lem2  32933  mdsymlem2  33011  cdj1i  33040  cgrahlb  33052  opreu2reuALT  33120  unidifsnne  33179  disjabrex  33223  disjabrexf  33224  acunirnmpt  33300  fgreu  33312  suppovss  33321  xrge0infss  33398  xrofsup  33405  fsumiunle  33466  mgcf1o  33610  xrge0addgt0  33624  fzto1st1  33709  cyc3genpm  33759  cycpmgcl  33760  submarchi  33793  archiabllem1  33800  archiabllem2a  33801  isarchiofld  33806  rlocval  33866  imaslmod  33960  lindfpropd  33983  unitprodclb  33990  drnglring  34070  dflring3  34075  dfufd2lem  34127  mplmulmvr  34217  lvecdim0  34285  constrmon  34422  constrextdg2  34427  locfinreflem  34518  zarcmplem  34559  rge0scvg  34627  lmxrge0  34630  lmdvg  34631  qqhval2  34660  esumrnmpt2  34746  esumfsup  34748  esumpcvgval  34756  esumcvg  34764  esumgect  34768  esumiun  34772  sigaclfu2  34799  sigainb  34815  insiga  34816  fiunelros  34853  measinblem  34899  measinb  34900  measdivcst  34903  measdivcstALTV  34904  omssubadd  34978  oddpwdc  35032  dstrvprob  35150  signsply0  35226  signstfvneq0  35247  bnj1408  35712  j0ltalephlem  35946  ptpconn  36084  sconnpi1  36090  resconn  36097  cvmliftmolem2  36133  cvmlift2lem12  36165  satfsschain  36215  satffunlem2lem1  36255  ifscgr  36901  cgrxfr  36912  outsideofeu  36988  linethru  37010  nmulcom  37035  nmuladdss  37054  neibastop1  37239  dnicn  37450  irrdifflemf  38339  irrdiff  38340  fin2so  38623  poimirlem28  38659  poimirlem31  38662  mblfinlem2  38669  mblfinlem3  38670  itg2addnclem  38682  ftc1anclem7  38710  ftc1anclem8  38711  ftc1anc  38712  ssbnd  38815  totbndbnd  38816  prtlem10  40015  lssats  40162  lkrlss  40245  lshpset2N  40269  2dim  40620  islvol5  40729  paddasslem11  40980  pexmidlem8N  41127  ltrnid  41285  idltrn  41300  trlator0  41321  trlnidatb  41327  cdlemf2  41712  cdlemg2cex  41741  tendodi1  41934  tendodi2  41935  diblss  42320  dihopelvalcpre  42398  dih1dimatlem  42479  dihglblem6  42490  primrootscoprmpow  43242  posbezout  43243  aks6d1c4  43267  sticksstones22  43311  aks6d1c6isolem1  43317  aks6d1c6isolem2  43318  aks6d1c6lem5  43320  grpods  43337  unitscyglem3  43340  unitscyglem4  43341  remul01  43551  sn-subeu  43571  sn-0tie0  43608  prjspertr  43726  prjspersym  43728  0prjspnrel  43756  mzpsubst  43852  mzpcompact2lem  43855  eldioph2  43866  eldioph2b  43867  diophren  43913  pell14qrexpcl  43967  elpell1qr2  43972  monotoddzzfi  44042  acongtr  44078  acongrep  44080  jm2.19lem4  44092  jm2.26a  44100  jm2.26lem3  44101  jm2.26  44102  isnumbasgrplem2  44199  mendassa  44285  omord2lim  44395  cantnftermord  44415  tfsconcatfv1  44434  tfsconcatfv2  44435  naddcnffo  44459  naddcnfcom  44461  naddcnfid1  44462  naddgeoa  44489  clsk3nimkb  45133  prmunb2  45388  4an4132  45575  fiiuncl  46175  ssinc  46195  ssdec  46196  supxrgelem  46442  infxr  46471  cvgcaule  46594  mullimc  46721  mullimcf  46728  neglimc  46750  climleltrp  46779  climisp  46849  limsupresxr  46869  liminfresxr  46870  liminflimsupclim  46910  xlimliminflimsup  46965  icccncfext  46990  cncfiooicclem1  46996  fprodcncf  47003  dvnprodlem3  47051  iblcncfioo  47081  itgspltprt  47082  stoweidlem7  47110  stoweidlem28  47131  stoweidlem34  47137  stoweidlem48  47151  stoweidlem52  47155  wallispilem3  47170  fourierdlem12  47222  fourierdlem38  47248  fourierdlem39  47249  fourierdlem42  47252  fourierdlem46  47255  fourierdlem48  47257  fourierdlem49  47258  fourierdlem50  47259  fourierdlem51  47260  fourierdlem65  47274  fourierdlem73  47282  fourierdlem76  47285  fourierdlem87  47296  fourierdlem103  47312  fourierdlem104  47313  sge0f1o  47485  sge0le  47510  sge0reuz  47550  ismeannd  47570  isomenndlem  47633  hoicvr  47651  hoidmvle  47703  smflimlem2  47875  smflimmpt  47913  fsupdm  47945  finfdm  47949  nndivides2  48547  imasetpreimafvbijlemf1  48579  nnsum4primeseven  48991  nnsum4primesevenALTV  48992  bgoldbtbndlem2  48997  bgoldbtbndlem3  48998  bgoldbtbnd  49000  isubgr3stgrlem6  49162  rrxlinec  49942  iccdisj  50105  upfval  50385  fullthinc  50678