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  7269  poseq  8163  oeeui  8597  oaabs2  8644  naddssim  8681  omxpenlem  9076  findcard3  9253  wemappo  9521  acndom2  10057  infpwfien  10065  sornom  10279  isf32lem2  10356  isf32lem4  10358  fin1a2lem11  10412  pwfseq  10667  gchina  10702  inttsk  10777  inar1  10778  prlem936  11050  mulcmpblnr  11074  00id  11403  mul02lem1  11404  addrid  11408  cnegex  11409  negeu  11465  add20  11744  ltmul12a  12089  lediv12a  12126  cru  12228  qextltlem  13246  xmullem  13308  xlemul1a  13332  ixxss12  13410  ioodisj  13527  elfz0fzfz0  13680  fsuppmapnn0fz  14052  seqf1o  14099  mulexpz  14158  leexp1a  14231  seqcoll  14521  swrdswrdlem  14765  pfxccatin12lem3  14793  sgnsub  15169  sgnmul  15170  abs3lem  15416  cau3lem  15432  climcau  15748  sumeq2ii  15770  climcndslem1  15929  climcndslem2  15930  geomulcvg  15956  mertenslem1  15964  mertenslem2  15965  mertens  15966  prodeq2ii  15991  prodmolem2  16015  bitsfzo  16518  sadadd2lem2  16533  dvdsmulgcd  16639  qredeu  16741  pc2dvds  16964  pcz  16966  ramcl  17114  firest  17510  mreexexlemd  17725  isacs2  17734  iscatd2  17762  ipodrsima  18622  mrelatlub  18643  mgmhmeql  18803  sgrppropd  18818  mndpropd  18846  mhmeql  18916  mhmid  19160  mhmmnd  19161  issubg4  19243  cycsubm  19304  cycsubmcom  19306  gasubg  19403  symgextf  19518  pmtr3ncom  19576  gexdvds  19685  oddvdssubg  19956  imasabl  19977  cyggeninv  19984  cyggenod  19985  submomnd  20233  issrg  20301  dvdsrmul1  20484  unitgrp  20498  cntzsubrng  20703  cntzsubr  20742  islmhm2  21196  lmhmeql  21213  lbspropd  21257  lssacsex  21305  rngqiprngimfo  21478  psgndiflemA  21788  isphl  21815  ocvocv  21858  lindfmm  22014  issubassa2  22079  mplbas2  22230  scmatmats  22705  smatvscl  22718  mdetdiag  22793  m2cpmfo  22950  pmatcollpw3fi1lem1  22980  pm2mpf1  22993  pm2mpghm  23010  fvmptnn04if  23043  chfacfscmulfsupp  23053  chfacfpmmulfsupp  23057  neissex  23321  neiptoptop  23325  neiptopnei  23326  restbas  23352  tgrest  23353  restopnb  23369  cnpco  23461  isreg2  23571  iunconn  23622  1stcrest  23647  2ndcctbss  23649  2ndcomap  23652  2ndcsep  23653  dislly  23691  kgencn2  23751  ptbasfi  23775  txhaus  23841  txkgen  23846  txconn  23883  qtopcn  23908  regr1lem2  23934  kqnrmlem1  23937  kqnrmlem2  23938  trfbas2  24037  trfil2  24081  flimcf  24176  hauspwpwf1  24181  fclscf  24219  flimfnfcls  24222  ustexsym  24410  ustuqtop4  24438  utop3cls  24445  utopreg  24446  ucnima  24474  ucncn  24478  metequiv2  24704  prdsxmslem2  24723  metcnpi3  24740  metustto  24747  metustid  24748  metustexhalf  24750  ngptgp  24830  xrsblre  25006  icccmp  25020  reconnlem1  25021  reconn  25023  opnreen  25026  metdsf  25043  metdscn  25051  mpomulcn  25063  fsumcn  25066  elcncf2  25086  cncfmet  25105  pcoass  25220  lmcau  25509  rrxdstprj1  25605  pmltpc  25646  ivthlem2  25648  ivthlem3  25649  ovollb2  25685  volsup  25752  ioombl1  25758  ioorf  25769  dyadss  25790  dyaddisjlem  25791  dyadmax  25794  volcn  25802  cncombf  25854  mbflimsup  25862  itg2const2  25937  iblss2  26002  cpnord  26131  dvmptfsum  26171  fta1g  26364  plydivex  26495  fta1  26506  aannenlem1  26528  ulmdvlem3  26602  advlogexp  26857  cxpmul2z  26893  atantayl2  27140  jensen  27190  isppw2  27316  lgsqr  27552  lgsqrmodndvds  27554  lgsdchrval  27555  lgsquad3  27588  2sqb  27633  dchrisumlem3  27692  pntrsumbnd2  27768  noinfbnd1lem5  27928  noetasuplem4  27937  noetainflem4  27941  noetalem1  27942  conway  28009  eqcuts3  28034  madebdayim  28118  madebdaylemlrcut  28129  negsprop  28265  mulscom  28369  absmuls  28474  bdayons  28506  addonbday  28509  bdayfinbndlem1  28697  remulscl  28732  tgjustf  28779  axsegcon  29314  axeuclidlem  29349  axcontlem9  29359  eengtrkg  29373  cusgrsize2inds  29840  pthdepisspth  30121  usgr2wlkneq  30142  crctcshwlkn0  30207  wpthswwlks2on  30350  clwwlkccatlem  30377  wwlksext2clwwlk  30445  umgr3v3e3cycl  30572  vdgn1frgrv2  30684  frgrwopreglem5  30709  frgrwopreg  30711  frgrhash2wsp  30720  numclwwlk1lem2fo  30746  vacn  31083  smcnlem  31086  0lno  31179  chocunii  31690  occl  31693  5oalem1  32043  3oalem2  32052  unoplin  32309  hmoplin  32331  lnconi  32422  kbass5  32509  mdslmd1lem1  32714  mdslmd1lem2  32715  mdsymlem2  32793  cdj1i  32822  opreu2reuALT  32860  unidifsnne  32919  disjabrex  32964  disjabrexf  32965  acunirnmpt  33041  fgreu  33053  suppovss  33063  xrge0infss  33142  xrofsup  33149  fsumiunle  33210  mgcf1o  33354  xrge0addgt0  33368  fzto1st1  33453  cyc3genpm  33503  cycpmgcl  33504  submarchi  33537  archiabllem1  33544  archiabllem2a  33545  isarchiofld  33550  rlocval  33610  imaslmod  33704  lindfpropd  33726  unitprodclb  33733  elrspunidl  33767  drnglring  33813  dflring3  33818  dfufd2lem  33870  mplmulmvr  33960  lvecdim0  34028  constrmon  34165  constrextdg2  34170  locfinreflem  34261  zarcmplem  34302  rge0scvg  34370  lmxrge0  34373  lmdvg  34374  qqhval2  34403  esumrnmpt2  34489  esumfsup  34491  esumpcvgval  34499  esumcvg  34507  esumgect  34511  esumiun  34515  sigaclfu2  34542  sigainb  34558  insiga  34559  fiunelros  34596  measinblem  34642  measinb  34643  measdivcst  34646  measdivcstALTV  34647  omssubadd  34722  oddpwdc  34776  dstrvprob  34894  signsply0  34970  signstfvneq0  34991  bnj1408  35456  ptpconn  35746  sconnpi1  35752  resconn  35759  cvmliftmolem2  35795  cvmlift2lem12  35827  satfsschain  35877  satffunlem2lem1  35917  ifscgr  36557  cgrxfr  36568  outsideofeu  36644  linethru  36666  nmulcom  36707  nmuladdss  36726  neibastop1  36911  dnicn  37122  irrdifflemf  38010  irrdiff  38011  fin2so  38299  matunitlindflem1  38308  matunitlindflem2  38309  poimirlem28  38340  poimirlem31  38343  mblfinlem2  38350  mblfinlem3  38351  itg2addnclem  38363  ftc1anclem7  38391  ftc1anclem8  38392  ftc1anc  38393  ssbnd  38480  totbndbnd  38481  prtlem10  39680  lssats  39827  lkrlss  39910  lshpset2N  39934  2dim  40285  islvol5  40394  paddasslem11  40645  pexmidlem8N  40792  ltrnid  40950  idltrn  40965  trlator0  40986  trlnidatb  40992  cdlemf2  41377  cdlemg2cex  41406  tendodi1  41599  tendodi2  41600  diblss  41985  dihopelvalcpre  42063  dih1dimatlem  42144  dihglblem6  42155  primrootscoprmpow  42907  posbezout  42908  aks6d1c4  42932  sticksstones22  42976  aks6d1c6isolem1  42982  aks6d1c6isolem2  42983  aks6d1c6lem5  42985  grpods  43002  unitscyglem3  43005  unitscyglem4  43006  remul01  43209  sn-subeu  43229  sn-0tie0  43266  prjspertr  43378  prjspersym  43380  0prjspnrel  43400  mzpsubst  43520  mzpcompact2lem  43523  eldioph2  43534  eldioph2b  43535  diophren  43581  pell14qrexpcl  43635  elpell1qr2  43640  monotoddzzfi  43710  acongtr  43746  acongrep  43748  jm2.19lem4  43760  jm2.26a  43768  jm2.26lem3  43769  jm2.26  43770  isnumbasgrplem2  43872  mendassa  43958  omord2lim  44068  cantnftermord  44088  tfsconcatfv1  44107  tfsconcatfv2  44108  naddcnffo  44132  naddcnfcom  44134  naddcnfid1  44135  naddgeoa  44162  clsk3nimkb  44807  prmunb2  45062  4an4132  45249  fiiuncl  45826  ssinc  45846  ssdec  45847  supxrgelem  46094  infxr  46123  cvgcaule  46246  mullimc  46373  mullimcf  46380  neglimc  46402  climleltrp  46431  climisp  46501  limsupresxr  46521  liminfresxr  46522  liminflimsupclim  46562  xlimliminflimsup  46617  icccncfext  46642  cncfiooicclem1  46648  fprodcncf  46655  dvnprodlem3  46703  iblcncfioo  46733  itgspltprt  46734  stoweidlem7  46762  stoweidlem28  46783  stoweidlem34  46789  stoweidlem48  46803  stoweidlem52  46807  wallispilem3  46822  fourierdlem12  46874  fourierdlem38  46900  fourierdlem39  46901  fourierdlem42  46904  fourierdlem46  46907  fourierdlem48  46909  fourierdlem49  46910  fourierdlem50  46911  fourierdlem51  46912  fourierdlem65  46926  fourierdlem73  46934  fourierdlem76  46937  fourierdlem87  46948  fourierdlem103  46964  fourierdlem104  46965  sge0f1o  47137  sge0le  47162  sge0reuz  47202  ismeannd  47222  isomenndlem  47285  hoicvr  47303  hoidmvle  47355  smflimlem2  47527  smflimmpt  47565  fsupdm  47597  finfdm  47601  nndivides2  48162  imasetpreimafvbijlemf1  48194  nnsum4primeseven  48606  nnsum4primesevenALTV  48607  bgoldbtbndlem2  48612  bgoldbtbndlem3  48613  bgoldbtbnd  48615  isubgr3stgrlem6  48777  rrxlinec  49557  iccdisj  49717  upfval  49995  fullthinc  50269