Theorem simplll 791

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  simp-4lOLD  802  f1imass  6715  oeeui  7889  oaabs2  7932  omxpenlem  8270  cantnfle  8785  acndom2  9130  infpwfien  9138  sornom  9354  isf32lem2  9431  isf32lem4  9433  fin1a2lem11  9487  ttukeylem5  9590  pwfseq  9741  gchina  9776  inttsk  9851  inar1  9852  prlem936  10124  mulcmpblnr  10147  00id  10467  mul02lem1  10468  addid1  10472  cnegex  10473  negeu  10527  add20  10796  ltmul12a  11135  lediv12a  11172  fiminre  11228  cru  11268  qextltlem  12238  xmullem  12299  xlemul1a  12323  ixxss12  12400  ioodisj  12512  elfz0fzfz0  12655  fsuppmapnn0fz  13006  seqf1o  13052  mulexpz  13110  leexp1a  13129  seqcoll  13452  swrdswrdlem  13694  abs3lem  14366  cau3lem  14382  climcau  14689  sumeq2ii  14711  summolem2  14735  climcndslem1  14868  climcndslem2  14869  geomulcvg  14894  mertenslem1  14902  mertenslem2  14903  mertens  14904  prodeq2ii  14929  prodmolem2  14951  bitsfzo  15441  sadadd2lem2  15456  dvdsmulgcd  15558  qredeu  15655  pc2dvds  15865  pcz  15867  ramcl  16015  firest  16362  mreexexlemd  16573  isacs2  16582  iscatd2  16610  ipodrsima  17434  mrelatlub  17455  mndpropd  17585  mhmeql  17633  isgrpinv  17742  mhmid  17806  mhmmnd  17807  issubg4  17880  gasubg  18001  symgextf  18103  pmtr3ncom  18161  gexdvds  18266  oddvdssubg  18527  cyggeninv  18554  cyggenod  18555  issrg  18777  dvdsrmul1  18923  unitgrp  18937  cntzsubr  19084  islmhm2  19313  lmhmeql  19330  lbspropd  19374  lssacsex  19420  issubassa2  19622  mplbas2  19747  psgndiflemA  20223  isphl  20251  ocvocv  20294  lindfmm  20445  scmatmats  20597  smatvscl  20610  mdetdiag  20685  m2cpmfo  20843  pmatcollpw3fi1lem1  20873  pm2mpf1  20886  pm2mpghm  20903  fvmptnn04if  20936  chfacfscmulfsupp  20946  chfacfpmmulfsupp  20950  neissex  21214  neiptoptop  21218  neiptopnei  21219  restbas  21245  tgrest  21246  restopnb  21262  cnpco  21354  isnrm3  21446  isreg2  21464  iunconn  21514  1stcrest  21539  2ndcctbss  21541  2ndcomap  21544  2ndcsep  21545  dislly  21583  kgencn2  21643  ptbasfi  21667  txhaus  21733  txkgen  21738  txconn  21775  qtopcn  21800  regr1lem2  21826  kqnrmlem1  21829  kqnrmlem2  21830  trfbas2  21929  trfil2  21973  flimcf  22068  hauspwpwf1  22073  fclscf  22111  flimfnfcls  22114  cnextcn  22153  ustexsym  22301  ustex2sym  22302  ustex3sym  22303  ustuqtop4  22330  utop3cls  22337  utopreg  22338  ucnima  22367  ucncn  22371  fmucnd  22378  metequiv2  22597  prdsxmslem2  22616  metcnpi3  22633  metustto  22640  metustid  22641  metustexhalf  22643  ngptgp  22722  xrsblre  22896  icccmp  22910  reconnlem1  22911  reconn  22913  opnreen  22916  metdsf  22933  metdscn  22941  fsumcn  22955  elcncf2  22975  cncfmet  22993  pcoass  23105  lmcau  23393  rrxdstprj1  23484  pmltpc  23511  ivthlem2  23513  ivthlem3  23514  ovollb2  23550  volsup  23617  ioombl1  23623  ioorf  23634  dyadss  23655  dyaddisjlem  23656  dyadmax  23659  volcn  23667  cncombf  23719  mbflimsup  23727  itg2const2  23802  iblss2  23866  cpnord  23992  dvmptfsum  24032  fta1g  24221  plydivex  24346  fta1  24357  aannenlem1  24377  ulmdvlem3  24450  abelthlem8  24487  pilem3OLD  24502  advlogexp  24695  cxpmul2z  24731  atantayl2  24959  jensen  25009  isppw2  25135  lgsqr  25370  lgsqrmodndvds  25372  lgsdchrval  25373  lgsquad3  25406  2sqb  25451  dchrisumlem3  25474  rpvmasum2  25495  mulog2sumlem2  25518  pntrsumbnd2  25550  f1otrg  26045  f1otrge  26046  axsegcon  26101  axeuclidlem  26136  axcontlem9  26146  eengtrkg  26159  cusgrsize2inds  26643  pthdepisspth  26926  usgr2wlkneq  26947  crctcshwlkn0  27009  wpthswwlks2on  27188  umgr3v3e3cycl  27465  vdgn1frgrv2  27579  frgrwopreglem5  27604  frgrwopreg  27606  frgrhash2wsp  27615  numclwwlk1lem2fo  27653  numclwwlk1lem2foOLD  27658  vacn  28008  smcnlem  28011  0lno  28104  chocunii  28619  occl  28622  5oalem1  28972  3oalem2  28981  unoplin  29238  hmoplin  29260  lnconi  29351  kbass5  29438  mdslmd1lem1  29643  mdslmd1lem2  29644  mdsymlem2  29722  cdj1i  29751  disjabrex  29846  disjabrexf  29847  acunirnmpt  29912  fgreu  29923  xrge0infss  29977  xrofsup  29985  fsumiunle  30027  xrge0addgt0  30141  submomnd  30160  submarchi  30190  archiabllem1  30197  archiabllem2a  30198  isarchiofld  30267  locfinreflem  30357  rge0scvg  30445  lmxrge0  30448  lmdvg  30449  qqhval2  30476  esumrnmpt2  30580  esumfsup  30582  esumpcvgval  30590  esumcvg  30598  esumgect  30602  esumiun  30606  sigaclfu2  30634  sigainb  30649  insiga  30650  fiunelros  30687  measinblem  30733  measinb  30734  measdivcstOLD  30737  measdivcst  30738  omssubadd  30812  oddpwdc  30866  dstrvprob  30984  sgnmul  31055  sgnsub  31057  signsply0  31080  signstfvneq0  31102  bnj1408  31555  ptpconn  31666  sconnpi1  31672  resconn  31679  cvmliftmolem2  31715  cvmlift2lem12  31747  poseq  32200  noetalem3  32312  noetalem5  32314  conway  32357  ifscgr  32598  cgrxfr  32609  outsideofeu  32685  linethru  32707  neibastop1  32800  dnicn  32924  fin2so  33823  matunitlindflem1  33832  matunitlindflem2  33833  poimirlem28  33864  poimirlem31  33867  mblfinlem2  33874  mblfinlem3  33875  itg2addnclem  33887  ftc1anclem7  33917  ftc1anclem8  33918  ftc1anc  33919  ssbnd  34012  totbndbnd  34013  prtlem10  34824  lssats  34971  lkrlss  35054  lshpset2N  35078  2dim  35429  islvol5  35538  paddasslem11  35789  pexmidlem8N  35936  ltrnid  36094  idltrn  36109  trlator0  36130  trlnidatb  36136  cdlemf2  36521  cdlemg2cex  36550  tendodi1  36743  tendodi2  36744  diblss  37129  dihopelvalcpre  37207  dih1dimatlem  37288  dihglblem6  37299  mzpsubst  37992  mzpcompact2lem  37995  eldioph2  38006  eldioph2b  38007  diophren  38058  pell14qrexpcl  38112  elpell1qr2  38117  monotoddzzfi  38187  acongtr  38225  acongrep  38227  jm2.19lem4  38239  jm2.26a  38247  jm2.26lem3  38248  jm2.26  38249  isnumbasgrplem2  38354  mendassa  38444  clsk3nimkb  39015  prmunb2  39187  4an4132  39380  fiiuncl  39888  ssinc  39918  ssdec  39919  supxrgelem  40194  infxr  40224  mullimc  40489  mullimcf  40496  neglimc  40520  climleltrp  40549  climisp  40619  limsupresxr  40639  liminfresxr  40640  liminflimsupclim  40680  icccncfext  40741  cncfiooicclem1  40747  fprodcncf  40755  dvnprodlem3  40804  iblcncfioo  40834  itgspltprt  40835  stoweidlem7  40864  stoweidlem28  40885  stoweidlem34  40891  stoweidlem48  40905  stoweidlem52  40909  wallispilem3  40924  fourierdlem12  40976  fourierdlem38  41002  fourierdlem39  41003  fourierdlem42  41006  fourierdlem46  41009  fourierdlem48  41011  fourierdlem49  41012  fourierdlem50  41013  fourierdlem51  41014  fourierdlem65  41028  fourierdlem73  41036  fourierdlem76  41039  fourierdlem87  41050  fourierdlem103  41066  fourierdlem104  41067  sge0f1o  41239  sge0le  41264  sge0reuz  41304  ismeannd  41324  isomenndlem  41387  hoicvr  41405  hoidmvle  41457  smflimlem2  41623  smflimmpt  41659  nnsum4primeseven  42367  nnsum4primesevenALTV  42368  bgoldbtbndlem2  42373  bgoldbtbndlem3  42374  bgoldbtbnd  42376  mgmhmeql  42475