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  7265  poseq  8160  oeeui  8594  oaabs2  8641  naddssim  8678  omxpenlem  9080  findcard3  9257  wemappo  9525  acndom2  10061  infpwfien  10069  sornom  10283  isf32lem2  10360  isf32lem4  10362  fin1a2lem11  10416  pwfseq  10677  gchina  10712  inttsk  10787  inar1  10788  prlem936  11060  mulcmpblnr  11084  00id  11413  mul02lem1  11414  addrid  11418  cnegex  11419  negeu  11475  add20  11754  ltmul12a  12099  lediv12a  12136  cru  12238  qextltlem  13258  xmullem  13320  xlemul1a  13344  ixxss12  13422  ioodisj  13539  elfz0fzfz0  13692  fsuppmapnn0fz  14064  seqf1o  14111  mulexpz  14170  leexp1a  14243  seqcoll  14533  swrdswrdlem  14777  pfxccatin12lem3  14805  s3rex  15025  sgnsub  15183  sgnmul  15184  abs3lem  15430  cau3lem  15446  climcau  15762  sumeq2ii  15784  climcndslem1  15942  climcndslem2  15943  geomulcvg  15969  mertenslem1  15977  mertenslem2  15978  mertens  15979  prodeq2ii  16004  prodmolem2  16028  bitsfzo  16531  sadadd2lem2  16546  dvdsmulgcd  16652  qredeu  16754  pc2dvds  16977  pcz  16979  ramcl  17127  firest  17523  mreexexlemd  17738  isacs2  17747  iscatd2  17775  ipodrsima  18635  mrelatlub  18656  mgmhmeql  18824  sgrppropd  18839  mndpropd  18870  mhmeql  18941  mhmid  19192  mhmmnd  19193  issubg4  19275  cycsubm  19336  cycsubmcom  19338  gasubg  19435  symgextf  19550  pmtr3ncom  19608  gexdvds  19717  oddvdssubg  19988  imasabl  20009  cyggeninv  20016  cyggenod  20017  submomnd  20265  issrg  20333  dvdsrmul1  20516  unitgrp  20530  cntzsubrng  20735  cntzsubr  20774  islmhm2  21228  lmhmeql  21245  lbspropd  21289  lssacsex  21337  rngqiprngimfo  21510  psgndiflemA  21820  isphl  21847  ocvocv  21890  lindfmm  22046  issubassa2  22113  mplbas2  22264  scmatmats  22739  smatvscl  22752  mdetdiag  22827  matunitlindflem1  22907  matunitlindflem2  22908  m2cpmfo  22987  pmatcollpw3fi1lem1  23017  pm2mpf1  23030  pm2mpghm  23047  fvmptnn04if  23080  chfacfscmulfsupp  23090  chfacfpmmulfsupp  23094  neissex  23358  neiptoptop  23362  neiptopnei  23363  restbas  23389  tgrest  23390  restopnb  23406  cnpco  23498  isreg2  23608  iunconn  23659  1stcrest  23684  2ndcctbss  23687  2ndcomap  23690  2ndcsep  23691  dislly  23729  kgencn2  23789  ptbasfi  23813  txhaus  23879  txkgen  23884  txconn  23921  qtopcn  23946  regr1lem2  23972  kqnrmlem1  23975  kqnrmlem2  23976  trfbas2  24075  trfil2  24119  flimcf  24214  hauspwpwf1  24219  fclscf  24257  flimfnfcls  24260  ustexsym  24448  ustuqtop4  24476  utop3cls  24483  utopreg  24484  ucnima  24512  ucncn  24516  metequiv2  24742  prdsxmslem2  24761  metcnpi3  24778  metustto  24785  metustid  24786  metustexhalf  24788  ngptgp  24868  xrsblre  25044  icccmp  25058  reconnlem1  25059  reconn  25061  opnreen  25064  metdsf  25081  metdscn  25089  mpomulcn  25101  fsumcn  25104  elcncf2  25124  cncfmet  25143  pcoass  25258  lmcau  25547  rrxdstprj1  25643  pmltpc  25684  ivthlem2  25686  ivthlem3  25687  ovollb2  25723  volsup  25790  ioombl1  25796  ioorf  25807  dyadss  25828  dyaddisjlem  25829  dyadmax  25832  volcn  25840  cncombf  25892  mbflimsup  25900  itg2const2  25975  iblss2  26040  cpnord  26169  dvmptfsum  26209  fta1g  26402  plydivex  26534  fta1  26545  aannenlem1  26571  ulmdvlem3  26645  advlogexp  26900  cxpmul2z  26936  atantayl2  27183  jensen  27233  isppw2  27359  lgsqr  27595  lgsqrmodndvds  27597  lgsdchrval  27598  lgsquad3  27631  2sqb  27676  dchrisumlem3  27735  pntrsumbnd2  27811  noinfbnd1lem5  27971  noetasuplem4  27980  noetainflem4  27984  noetalem1  27985  conway  28052  eqcuts3  28077  madebdayim  28161  madebdaylemlrcut  28172  negsprop  28308  mulscom  28412  absmuls  28517  bdayons  28549  addonbday  28552  bdayfinbndlem1  28740  remulscl  28775  tgjustf  28822  axsegcon  29392  axeuclidlem  29427  axcontlem9  29437  eengtrkg  29451  cusgrsize2inds  29921  pthdepisspth  30208  usgr2wlkneq  30229  crctcshwlkn0  30297  wpthswwlks2on  30440  clwwlkccatlem  30467  wwlksext2clwwlk  30535  umgr3v3e3cycl  30672  vdgn1frgrv2  30784  frgrwopreglem5  30809  frgrwopreg  30811  frgrhash2wsp  30820  numclwwlk1lem2fo  30846  vacn  31183  smcnlem  31186  0lno  31279  chocunii  31790  occl  31793  5oalem1  32143  3oalem2  32152  unoplin  32409  hmoplin  32431  lnconi  32522  kbass5  32609  mdslmd1lem1  32814  mdslmd1lem2  32815  mdsymlem2  32893  cdj1i  32922  opreu2reuALT  32960  unidifsnne  33019  disjabrex  33063  disjabrexf  33064  acunirnmpt  33140  fgreu  33152  suppovss  33161  xrge0infss  33239  xrofsup  33246  fsumiunle  33307  mgcf1o  33451  xrge0addgt0  33465  fzto1st1  33550  cyc3genpm  33600  cycpmgcl  33601  submarchi  33634  archiabllem1  33641  archiabllem2a  33642  isarchiofld  33647  rlocval  33707  imaslmod  33801  lindfpropd  33823  unitprodclb  33830  elrspunidl  33864  drnglring  33910  dflring3  33915  dfufd2lem  33967  mplmulmvr  34057  lvecdim0  34125  constrmon  34262  constrextdg2  34267  locfinreflem  34358  zarcmplem  34399  rge0scvg  34467  lmxrge0  34470  lmdvg  34471  qqhval2  34500  esumrnmpt2  34586  esumfsup  34588  esumpcvgval  34596  esumcvg  34604  esumgect  34608  esumiun  34612  sigaclfu2  34639  sigainb  34655  insiga  34656  fiunelros  34693  measinblem  34739  measinb  34740  measdivcst  34743  measdivcstALTV  34744  omssubadd  34819  oddpwdc  34873  dstrvprob  34991  signsply0  35067  signstfvneq0  35088  bnj1408  35553  ptpconn  35820  sconnpi1  35826  resconn  35833  cvmliftmolem2  35869  cvmlift2lem12  35901  satfsschain  35951  satffunlem2lem1  35991  ifscgr  36632  cgrxfr  36643  outsideofeu  36719  linethru  36741  nmulcom  36782  nmuladdss  36801  neibastop1  36986  dnicn  37197  irrdifflemf  38085  irrdiff  38086  fin2so  38369  poimirlem28  38405  poimirlem31  38408  mblfinlem2  38415  mblfinlem3  38416  itg2addnclem  38428  ftc1anclem7  38456  ftc1anclem8  38457  ftc1anc  38458  ssbnd  38546  totbndbnd  38547  prtlem10  39746  lssats  39893  lkrlss  39976  lshpset2N  40000  2dim  40351  islvol5  40460  paddasslem11  40711  pexmidlem8N  40858  ltrnid  41016  idltrn  41031  trlator0  41052  trlnidatb  41058  cdlemf2  41443  cdlemg2cex  41472  tendodi1  41665  tendodi2  41666  diblss  42051  dihopelvalcpre  42129  dih1dimatlem  42210  dihglblem6  42221  primrootscoprmpow  42973  posbezout  42974  aks6d1c4  42998  sticksstones22  43042  aks6d1c6isolem1  43048  aks6d1c6isolem2  43049  aks6d1c6lem5  43051  grpods  43068  unitscyglem3  43071  unitscyglem4  43072  remul01  43290  sn-subeu  43310  sn-0tie0  43347  prjspertr  43459  prjspersym  43461  0prjspnrel  43481  mzpsubst  43601  mzpcompact2lem  43604  eldioph2  43615  eldioph2b  43616  diophren  43662  pell14qrexpcl  43716  elpell1qr2  43721  monotoddzzfi  43791  acongtr  43827  acongrep  43829  jm2.19lem4  43841  jm2.26a  43849  jm2.26lem3  43850  jm2.26  43851  isnumbasgrplem2  43953  mendassa  44039  omord2lim  44149  cantnftermord  44169  tfsconcatfv1  44188  tfsconcatfv2  44189  naddcnffo  44213  naddcnfcom  44215  naddcnfid1  44216  naddgeoa  44243  clsk3nimkb  44888  prmunb2  45143  4an4132  45330  fiiuncl  45907  ssinc  45927  ssdec  45928  supxrgelem  46175  infxr  46204  cvgcaule  46327  mullimc  46454  mullimcf  46461  neglimc  46483  climleltrp  46512  climisp  46582  limsupresxr  46602  liminfresxr  46603  liminflimsupclim  46643  xlimliminflimsup  46698  icccncfext  46723  cncfiooicclem1  46729  fprodcncf  46736  dvnprodlem3  46784  iblcncfioo  46814  itgspltprt  46815  stoweidlem7  46843  stoweidlem28  46864  stoweidlem34  46870  stoweidlem48  46884  stoweidlem52  46888  wallispilem3  46903  fourierdlem12  46955  fourierdlem38  46981  fourierdlem39  46982  fourierdlem42  46985  fourierdlem46  46988  fourierdlem48  46990  fourierdlem49  46991  fourierdlem50  46992  fourierdlem51  46993  fourierdlem65  47007  fourierdlem73  47015  fourierdlem76  47018  fourierdlem87  47029  fourierdlem103  47045  fourierdlem104  47046  sge0f1o  47218  sge0le  47243  sge0reuz  47283  ismeannd  47303  isomenndlem  47366  hoicvr  47384  hoidmvle  47436  smflimlem2  47608  smflimmpt  47646  fsupdm  47678  finfdm  47682  nndivides2  48280  imasetpreimafvbijlemf1  48312  nnsum4primeseven  48724  nnsum4primesevenALTV  48725  bgoldbtbndlem2  48730  bgoldbtbndlem3  48731  bgoldbtbnd  48733  isubgr3stgrlem6  48895  rrxlinec  49674  iccdisj  49832  upfval  50110  fullthinc  50384