Theorem simplll 780

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  f1imass  7215  poseq  8105  oeeui  8535  oaabs2  8582  naddssim  8618  omxpenlem  9013  findcard3  9190  wemappo  9461  acndom2  9974  infpwfien  9982  sornom  10197  isf32lem2  10274  isf32lem4  10276  fin1a2lem11  10330  pwfseq  10585  gchina  10620  inttsk  10695  inar1  10696  prlem936  10968  mulcmpblnr  10992  00id  11319  mul02lem1  11320  addrid  11324  cnegex  11325  negeu  11381  add20  11660  ltmul12a  12009  lediv12a  12047  cru  12149  qextltlem  13152  xmullem  13214  xlemul1a  13238  ixxss12  13316  ioodisj  13433  elfz0fzfz0  13585  fsuppmapnn0fz  13956  seqf1o  14003  mulexpz  14062  leexp1a  14135  seqcoll  14424  swrdswrdlem  14664  pfxccatin12lem3  14692  abs3lem  15299  cau3lem  15315  climcau  15631  sumeq2ii  15653  climcndslem1  15812  climcndslem2  15813  geomulcvg  15839  mertenslem1  15847  mertenslem2  15848  mertens  15849  prodeq2ii  15874  prodmolem2  15898  bitsfzo  16402  sadadd2lem2  16417  dvdsmulgcd  16523  qredeu  16625  pc2dvds  16848  pcz  16850  ramcl  16998  firest  17393  mreexexlemd  17608  isacs2  17617  iscatd2  17645  ipodrsima  18505  mrelatlub  18526  mgmhmeql  18682  sgrppropd  18697  mndpropd  18725  mhmeql  18792  mhmid  19037  mhmmnd  19038  issubg4  19119  cycsubm  19175  cycsubmcom  19177  gasubg  19275  symgextf  19390  pmtr3ncom  19448  gexdvds  19557  oddvdssubg  19828  imasabl  19849  cyggeninv  19856  cyggenod  19857  submomnd  20105  issrg  20167  dvdsrmul1  20347  unitgrp  20361  cntzsubrng  20546  cntzsubr  20585  islmhm2  21035  lmhmeql  21052  lbspropd  21096  lssacsex  21144  rngqiprngimfo  21301  psgndiflemA  21583  isphl  21610  ocvocv  21653  lindfmm  21809  issubassa2  21874  mplbas2  22025  scmatmats  22501  smatvscl  22514  mdetdiag  22589  m2cpmfo  22746  pmatcollpw3fi1lem1  22776  pm2mpf1  22789  pm2mpghm  22806  fvmptnn04if  22839  chfacfscmulfsupp  22849  chfacfpmmulfsupp  22853  neissex  23117  neiptoptop  23121  neiptopnei  23122  restbas  23148  tgrest  23149  restopnb  23165  cnpco  23257  isreg2  23367  iunconn  23418  1stcrest  23443  2ndcctbss  23445  2ndcomap  23448  2ndcsep  23449  dislly  23487  kgencn2  23547  ptbasfi  23571  txhaus  23637  txkgen  23642  txconn  23679  qtopcn  23704  regr1lem2  23730  kqnrmlem1  23733  kqnrmlem2  23734  trfbas2  23833  trfil2  23877  flimcf  23972  hauspwpwf1  23977  fclscf  24015  flimfnfcls  24018  ustexsym  24206  ustuqtop4  24234  utop3cls  24241  utopreg  24242  ucnima  24270  ucncn  24274  metequiv2  24500  prdsxmslem2  24519  metcnpi3  24536  metustto  24543  metustid  24544  metustexhalf  24546  ngptgp  24626  xrsblre  24802  icccmp  24816  reconnlem1  24817  reconn  24819  opnreen  24822  metdsf  24839  metdscn  24847  mpomulcn  24859  fsumcn  24862  elcncf2  24882  cncfmet  24901  pcoass  25016  lmcau  25305  rrxdstprj1  25401  pmltpc  25442  ivthlem2  25444  ivthlem3  25445  ovollb2  25481  volsup  25548  ioombl1  25554  ioorf  25565  dyadss  25586  dyaddisjlem  25587  dyadmax  25590  volcn  25598  cncombf  25650  mbflimsup  25658  itg2const2  25733  iblss2  25798  cpnord  25927  dvmptfsum  25967  fta1g  26160  plydivex  26288  fta1  26299  aannenlem1  26319  ulmdvlem3  26392  advlogexp  26644  cxpmul2z  26680  atantayl2  26927  jensen  26977  isppw2  27103  lgsqr  27339  lgsqrmodndvds  27341  lgsdchrval  27342  lgsquad3  27375  2sqb  27420  dchrisumlem3  27479  pntrsumbnd2  27555  noinfbnd1lem5  27716  noetasuplem4  27725  noetainflem4  27729  noetalem1  27730  conway  27796  eqcuts3  27821  madebdayim  27905  madebdaylemlrcut  27916  negsprop  28052  mulscom  28156  absmuls  28261  bdayons  28293  addonbday  28296  bdayfinbndlem1  28484  remulscl  28519  tgjustf  28566  axsegcon  29021  axeuclidlem  29056  axcontlem9  29066  eengtrkg  29080  cusgrsize2inds  29547  pthdepisspth  29828  usgr2wlkneq  29849  crctcshwlkn0  29914  wpthswwlks2on  30057  clwwlkccatlem  30084  wwlksext2clwwlk  30152  umgr3v3e3cycl  30279  vdgn1frgrv2  30391  frgrwopreglem5  30416  frgrwopreg  30418  frgrhash2wsp  30427  numclwwlk1lem2fo  30453  vacn  30790  smcnlem  30793  0lno  30886  chocunii  31397  occl  31400  5oalem1  31750  3oalem2  31759  unoplin  32016  hmoplin  32038  lnconi  32129  kbass5  32216  mdslmd1lem1  32421  mdslmd1lem2  32422  mdsymlem2  32500  cdj1i  32529  opreu2reuALT  32571  unidifsnne  32631  disjabrex  32678  disjabrexf  32679  acunirnmpt  32758  fgreu  32770  suppovss  32780  xrge0infss  32859  xrofsup  32866  fsumiunle  32928  sgnmul  32934  sgnsub  32936  mgcf1o  33089  xrge0addgt0  33103  fzto1st1  33190  cyc3genpm  33240  cycpmgcl  33241  submarchi  33274  archiabllem1  33281  archiabllem2a  33282  isarchiofld  33287  rlocval  33347  imaslmod  33443  lindfpropd  33472  unitprodclb  33479  elrspunidl  33518  dfufd2lem  33639  mplmulmvr  33730  lvecdim0  33798  constrmon  33935  constrextdg2  33940  locfinreflem  34031  zarcmplem  34072  rge0scvg  34140  lmxrge0  34143  lmdvg  34144  qqhval2  34173  esumrnmpt2  34259  esumfsup  34261  esumpcvgval  34269  esumcvg  34277  esumgect  34281  esumiun  34285  sigaclfu2  34312  sigainb  34327  insiga  34328  fiunelros  34365  measinblem  34411  measinb  34412  measdivcst  34415  measdivcstALTV  34416  omssubadd  34491  oddpwdc  34545  dstrvprob  34663  signsply0  34742  signstfvneq0  34763  bnj1408  35225  ptpconn  35468  sconnpi1  35474  resconn  35481  cvmliftmolem2  35517  cvmlift2lem12  35549  satfsschain  35599  satffunlem2lem1  35639  ifscgr  36279  cgrxfr  36290  outsideofeu  36366  linethru  36388  neibastop1  36594  dnicn  36805  irrdifflemf  37692  irrdiff  37693  fin2so  37981  matunitlindflem1  37990  matunitlindflem2  37991  poimirlem28  38022  poimirlem31  38025  mblfinlem2  38032  mblfinlem3  38033  itg2addnclem  38045  ftc1anclem7  38073  ftc1anclem8  38074  ftc1anc  38075  ssbnd  38162  totbndbnd  38163  prtlem10  39364  lssats  39511  lkrlss  39594  lshpset2N  39618  2dim  39969  islvol5  40078  paddasslem11  40329  pexmidlem8N  40476  ltrnid  40634  idltrn  40649  trlator0  40670  trlnidatb  40676  cdlemf2  41061  cdlemg2cex  41090  tendodi1  41283  tendodi2  41284  diblss  41669  dihopelvalcpre  41747  dih1dimatlem  41828  dihglblem6  41839  primrootscoprmpow  42591  posbezout  42592  aks6d1c4  42616  sticksstones22  42660  aks6d1c6isolem1  42666  aks6d1c6isolem2  42667  aks6d1c6lem5  42669  grpods  42686  unitscyglem3  42689  unitscyglem4  42690  remul01  42891  sn-subeu  42911  sn-0tie0  42948  prjspertr  43062  prjspersym  43064  0prjspnrel  43084  mzpsubst  43204  mzpcompact2lem  43207  eldioph2  43218  eldioph2b  43219  diophren  43265  pell14qrexpcl  43319  elpell1qr2  43324  monotoddzzfi  43394  acongtr  43430  acongrep  43432  jm2.19lem4  43444  jm2.26a  43452  jm2.26lem3  43453  jm2.26  43454  isnumbasgrplem2  43556  mendassa  43642  omord2lim  43752  cantnftermord  43772  tfsconcatfv1  43791  tfsconcatfv2  43792  naddcnffo  43816  naddcnfcom  43818  naddcnfid1  43819  naddgeoa  43846  clsk3nimkb  44491  prmunb2  44762  4an4132  44950  fiiuncl  45520  ssinc  45541  ssdec  45542  supxrgelem  45789  infxr  45818  cvgcaule  45941  mullimc  46068  mullimcf  46075  neglimc  46097  climleltrp  46126  climisp  46196  limsupresxr  46216  liminfresxr  46217  liminflimsupclim  46257  xlimliminflimsup  46312  icccncfext  46337  cncfiooicclem1  46343  fprodcncf  46350  dvnprodlem3  46398  iblcncfioo  46428  itgspltprt  46429  stoweidlem7  46457  stoweidlem28  46478  stoweidlem34  46484  stoweidlem48  46498  stoweidlem52  46502  wallispilem3  46517  fourierdlem12  46569  fourierdlem38  46595  fourierdlem39  46596  fourierdlem42  46599  fourierdlem46  46602  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  fourierdlem51  46607  fourierdlem65  46621  fourierdlem73  46629  fourierdlem76  46632  fourierdlem87  46643  fourierdlem103  46659  fourierdlem104  46660  sge0f1o  46832  sge0le  46857  sge0reuz  46897  ismeannd  46917  isomenndlem  46980  hoicvr  46998  hoidmvle  47050  smflimlem2  47222  smflimmpt  47260  fsupdm  47292  finfdm  47296  nndivides2  47854  imasetpreimafvbijlemf1  47886  nnsum4primeseven  48298  nnsum4primesevenALTV  48299  bgoldbtbndlem2  48304  bgoldbtbndlem3  48305  bgoldbtbnd  48307  isubgr3stgrlem6  48469  rrxlinec  49234  iccdisj  49395  upfval  49673  fullthinc  49947