Theorem simplll 771

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 726	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 206  df-an 396

This theorem is referenced by:  f1imass  7131  oeeui  8409  oaabs2  8453  omxpenlem  8829  wemappo  9269  acndom2  9794  infpwfien  9802  sornom  10017  isf32lem2  10094  isf32lem4  10096  fin1a2lem11  10150  pwfseq  10404  gchina  10439  inttsk  10514  inar1  10515  prlem936  10787  mulcmpblnr  10811  00id  11133  mul02lem1  11134  addid1  11138  cnegex  11139  negeu  11194  add20  11470  ltmul12a  11814  lediv12a  11851  cru  11948  qextltlem  12918  xmullem  12980  xlemul1a  13004  ixxss12  13081  ioodisj  13196  elfz0fzfz0  13343  fsuppmapnn0fz  13697  seqf1o  13745  mulexpz  13804  leexp1a  13874  seqcoll  14159  swrdswrdlem  14398  pfxccatin12lem3  14426  abs3lem  15031  cau3lem  15047  climcau  15363  sumeq2ii  15386  climcndslem1  15542  climcndslem2  15543  geomulcvg  15569  mertenslem1  15577  mertenslem2  15578  mertens  15579  prodeq2ii  15604  prodmolem2  15626  bitsfzo  16123  sadadd2lem2  16138  dvdsmulgcd  16246  qredeu  16344  pc2dvds  16561  pcz  16563  ramcl  16711  firest  17124  mreexexlemd  17334  isacs2  17343  iscatd2  17371  ipodrsima  18240  mrelatlub  18261  mndpropd  18391  mhmeql  18445  mhmid  18677  mhmmnd  18678  issubg4  18755  cycsubm  18802  cycsubmcom  18804  gasubg  18889  symgextf  19006  pmtr3ncom  19064  gexdvds  19170  oddvdssubg  19437  cyggeninv  19464  cyggenod  19465  issrg  19724  dvdsrmul1  19876  unitgrp  19890  cntzsubr  20038  islmhm2  20281  lmhmeql  20298  lbspropd  20342  lssacsex  20387  psgndiflemA  20787  isphl  20814  ocvocv  20857  lindfmm  21015  issubassa2  21077  mplbas2  21224  scmatmats  21641  smatvscl  21654  mdetdiag  21729  m2cpmfo  21886  pmatcollpw3fi1lem1  21916  pm2mpf1  21929  pm2mpghm  21946  fvmptnn04if  21979  chfacfscmulfsupp  21989  chfacfpmmulfsupp  21993  neissex  22259  neiptoptop  22263  neiptopnei  22264  restbas  22290  tgrest  22291  restopnb  22307  cnpco  22399  isreg2  22509  iunconn  22560  1stcrest  22585  2ndcctbss  22587  2ndcomap  22590  2ndcsep  22591  dislly  22629  kgencn2  22689  ptbasfi  22713  txhaus  22779  txkgen  22784  txconn  22821  qtopcn  22846  regr1lem2  22872  kqnrmlem1  22875  kqnrmlem2  22876  trfbas2  22975  trfil2  23019  flimcf  23114  hauspwpwf1  23119  fclscf  23157  flimfnfcls  23160  ustexsym  23348  ustuqtop4  23377  utop3cls  23384  utopreg  23385  ucnima  23414  ucncn  23418  metequiv2  23647  prdsxmslem2  23666  metcnpi3  23683  metustto  23690  metustid  23691  metustexhalf  23693  ngptgp  23773  xrsblre  23955  icccmp  23969  reconnlem1  23970  reconn  23972  opnreen  23975  metdsf  23992  metdscn  24000  fsumcn  24014  elcncf2  24034  cncfmet  24053  pcoass  24168  lmcau  24458  rrxdstprj1  24554  pmltpc  24595  ivthlem2  24597  ivthlem3  24598  ovollb2  24634  volsup  24701  ioombl1  24707  ioorf  24718  dyadss  24739  dyaddisjlem  24740  dyadmax  24743  volcn  24751  cncombf  24803  mbflimsup  24811  itg2const2  24887  iblss2  24951  cpnord  25080  dvmptfsum  25120  fta1g  25313  plydivex  25438  fta1  25449  aannenlem1  25469  ulmdvlem3  25542  advlogexp  25791  cxpmul2z  25827  atantayl2  26069  jensen  26119  isppw2  26245  lgsqr  26480  lgsqrmodndvds  26482  lgsdchrval  26483  lgsquad3  26516  2sqb  26561  dchrisumlem3  26620  pntrsumbnd2  26696  tgjustf  26815  axsegcon  27276  axeuclidlem  27311  axcontlem9  27321  eengtrkg  27335  cusgrsize2inds  27801  pthdepisspth  28082  usgr2wlkneq  28103  crctcshwlkn0  28165  wpthswwlks2on  28305  clwwlkccatlem  28332  wwlksext2clwwlk  28400  umgr3v3e3cycl  28527  vdgn1frgrv2  28639  frgrwopreglem5  28664  frgrwopreg  28666  frgrhash2wsp  28675  numclwwlk1lem2fo  28701  vacn  29035  smcnlem  29038  0lno  29131  chocunii  29642  occl  29645  5oalem1  29995  3oalem2  30004  unoplin  30261  hmoplin  30283  lnconi  30374  kbass5  30461  mdslmd1lem1  30666  mdslmd1lem2  30667  mdsymlem2  30745  cdj1i  30774  opreu2reuALT  30804  unidifsnne  30863  disjabrex  30900  disjabrexf  30901  acunirnmpt  30975  fgreu  30988  suppovss  30996  xrge0infss  31062  xrofsup  31069  fsumiunle  31122  mgcf1o  31260  xrge0addgt0  31279  submomnd  31315  fzto1st1  31348  cyc3genpm  31398  cycpmgcl  31399  submarchi  31419  archiabllem1  31426  archiabllem2a  31427  isarchiofld  31495  imaslmod  31532  lindfpropd  31555  elrspunidl  31585  lvecdim0  31669  locfinreflem  31769  zarcmplem  31810  rge0scvg  31878  lmxrge0  31881  lmdvg  31882  qqhval2  31911  esumrnmpt2  32015  esumfsup  32017  esumpcvgval  32025  esumcvg  32033  esumgect  32037  esumiun  32041  sigaclfu2  32068  sigainb  32083  insiga  32084  fiunelros  32121  measinblem  32167  measinb  32168  measdivcst  32171  measdivcstALTV  32172  omssubadd  32246  oddpwdc  32300  dstrvprob  32417  sgnmul  32488  sgnsub  32490  signsply0  32509  signstfvneq0  32530  bnj1408  32995  ptpconn  33174  sconnpi1  33180  resconn  33187  cvmliftmolem2  33223  cvmlift2lem12  33255  satfsschain  33305  satffunlem2lem1  33345  poseq  33781  naddssim  33816  noinfbnd1lem5  33909  noetasuplem4  33918  noetainflem4  33922  noetalem1  33923  conway  33972  madebdayim  34049  madebdaylemlrcut  34058  ifscgr  34325  cgrxfr  34336  outsideofeu  34412  linethru  34434  neibastop1  34527  dnicn  34651  irrdifflemf  35475  irrdiff  35476  fin2so  35743  matunitlindflem1  35752  matunitlindflem2  35753  poimirlem28  35784  poimirlem31  35787  mblfinlem2  35794  mblfinlem3  35795  itg2addnclem  35807  ftc1anclem7  35835  ftc1anclem8  35836  ftc1anc  35837  ssbnd  35925  totbndbnd  35926  prtlem10  36858  lssats  37005  lkrlss  37088  lshpset2N  37112  2dim  37463  islvol5  37572  paddasslem11  37823  pexmidlem8N  37970  ltrnid  38128  idltrn  38143  trlator0  38164  trlnidatb  38170  cdlemf2  38555  cdlemg2cex  38584  tendodi1  38777  tendodi2  38778  diblss  39163  dihopelvalcpre  39241  dih1dimatlem  39322  dihglblem6  39333  sticksstones22  40104  remul01  40370  sn-subeu  40388  sn-0tie0  40401  itrere  40416  retire  40417  prjspertr  40424  prjspersym  40426  0prjspnrel  40444  mzpsubst  40550  mzpcompact2lem  40553  eldioph2  40564  eldioph2b  40565  diophren  40615  pell14qrexpcl  40669  elpell1qr2  40674  monotoddzzfi  40744  acongtr  40780  acongrep  40782  jm2.19lem4  40794  jm2.26a  40802  jm2.26lem3  40803  jm2.26  40804  isnumbasgrplem2  40909  mendassa  40999  clsk3nimkb  41603  prmunb2  41882  4an4132  42072  fiiuncl  42566  ssinc  42590  ssdec  42591  supxrgelem  42830  infxr  42860  mullimc  43111  mullimcf  43118  neglimc  43142  climleltrp  43171  climisp  43241  limsupresxr  43261  liminfresxr  43262  liminflimsupclim  43302  xlimliminflimsup  43357  icccncfext  43382  cncfiooicclem1  43388  fprodcncf  43395  dvnprodlem3  43443  iblcncfioo  43473  itgspltprt  43474  stoweidlem7  43502  stoweidlem28  43523  stoweidlem34  43529  stoweidlem48  43543  stoweidlem52  43547  wallispilem3  43562  fourierdlem12  43614  fourierdlem38  43640  fourierdlem39  43641  fourierdlem42  43644  fourierdlem46  43647  fourierdlem48  43649  fourierdlem49  43650  fourierdlem50  43651  fourierdlem51  43652  fourierdlem65  43666  fourierdlem73  43674  fourierdlem76  43677  fourierdlem87  43688  fourierdlem103  43704  fourierdlem104  43705  sge0f1o  43874  sge0le  43899  sge0reuz  43939  ismeannd  43959  isomenndlem  44022  hoicvr  44040  hoidmvle  44092  smflimlem2  44258  smflimmpt  44294  imasetpreimafvbijlemf1  44808  nnsum4primeseven  45204  nnsum4primesevenALTV  45205  bgoldbtbndlem2  45210  bgoldbtbndlem3  45211  bgoldbtbnd  45213  isomuspgrlem2  45237  mgmhmeql  45309  rrxlinec  46034  iccdisj  46144  fullthinc  46279