Theorem simplll 774

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 729	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 207  df-an 396

This theorem is referenced by:  f1imass  7301  poseq  8199  oeeui  8658  oaabs2  8705  naddssim  8741  omxpenlem  9139  findcard3  9346  wemappo  9618  acndom2  10123  infpwfien  10131  sornom  10346  isf32lem2  10423  isf32lem4  10425  fin1a2lem11  10479  pwfseq  10733  gchina  10768  inttsk  10843  inar1  10844  prlem936  11116  mulcmpblnr  11140  00id  11465  mul02lem1  11466  addrid  11470  cnegex  11471  negeu  11526  add20  11802  ltmul12a  12150  lediv12a  12188  cru  12285  qextltlem  13264  xmullem  13326  xlemul1a  13350  ixxss12  13427  ioodisj  13542  elfz0fzfz0  13690  fsuppmapnn0fz  14047  seqf1o  14094  mulexpz  14153  leexp1a  14225  seqcoll  14513  swrdswrdlem  14752  pfxccatin12lem3  14780  abs3lem  15387  cau3lem  15403  climcau  15719  sumeq2ii  15741  climcndslem1  15897  climcndslem2  15898  geomulcvg  15924  mertenslem1  15932  mertenslem2  15933  mertens  15934  prodeq2ii  15959  prodmolem2  15983  bitsfzo  16481  sadadd2lem2  16496  dvdsmulgcd  16603  qredeu  16705  pc2dvds  16926  pcz  16928  ramcl  17076  firest  17492  mreexexlemd  17702  isacs2  17711  iscatd2  17739  ipodrsima  18611  mrelatlub  18632  mgmhmeql  18754  sgrppropd  18769  mndpropd  18797  mhmeql  18861  mhmid  19103  mhmmnd  19104  issubg4  19185  cycsubm  19242  cycsubmcom  19244  gasubg  19342  symgextf  19459  pmtr3ncom  19517  gexdvds  19626  oddvdssubg  19897  imasabl  19918  cyggeninv  19925  cyggenod  19926  issrg  20215  dvdsrmul1  20395  unitgrp  20409  cntzsubrng  20593  cntzsubr  20634  islmhm2  21060  lmhmeql  21077  lbspropd  21121  lssacsex  21169  rngqiprngimfo  21334  psgndiflemA  21642  isphl  21669  ocvocv  21712  lindfmm  21870  issubassa2  21935  mplbas2  22083  scmatmats  22538  smatvscl  22551  mdetdiag  22626  m2cpmfo  22783  pmatcollpw3fi1lem1  22813  pm2mpf1  22826  pm2mpghm  22843  fvmptnn04if  22876  chfacfscmulfsupp  22886  chfacfpmmulfsupp  22890  neissex  23156  neiptoptop  23160  neiptopnei  23161  restbas  23187  tgrest  23188  restopnb  23204  cnpco  23296  isreg2  23406  iunconn  23457  1stcrest  23482  2ndcctbss  23484  2ndcomap  23487  2ndcsep  23488  dislly  23526  kgencn2  23586  ptbasfi  23610  txhaus  23676  txkgen  23681  txconn  23718  qtopcn  23743  regr1lem2  23769  kqnrmlem1  23772  kqnrmlem2  23773  trfbas2  23872  trfil2  23916  flimcf  24011  hauspwpwf1  24016  fclscf  24054  flimfnfcls  24057  ustexsym  24245  ustuqtop4  24274  utop3cls  24281  utopreg  24282  ucnima  24311  ucncn  24315  metequiv2  24544  prdsxmslem2  24563  metcnpi3  24580  metustto  24587  metustid  24588  metustexhalf  24590  ngptgp  24670  xrsblre  24852  icccmp  24866  reconnlem1  24867  reconn  24869  opnreen  24872  metdsf  24889  metdscn  24897  mpomulcn  24910  fsumcn  24913  elcncf2  24935  cncfmet  24954  pcoass  25076  lmcau  25366  rrxdstprj1  25462  pmltpc  25504  ivthlem2  25506  ivthlem3  25507  ovollb2  25543  volsup  25610  ioombl1  25616  ioorf  25627  dyadss  25648  dyaddisjlem  25649  dyadmax  25652  volcn  25660  cncombf  25712  mbflimsup  25720  itg2const2  25796  iblss2  25861  cpnord  25991  dvmptfsum  26033  fta1g  26229  plydivex  26357  fta1  26368  aannenlem1  26388  ulmdvlem3  26463  advlogexp  26715  cxpmul2z  26751  atantayl2  26999  jensen  27050  isppw2  27176  lgsqr  27413  lgsqrmodndvds  27415  lgsdchrval  27416  lgsquad3  27449  2sqb  27494  dchrisumlem3  27553  pntrsumbnd2  27629  noinfbnd1lem5  27790  noetasuplem4  27799  noetainflem4  27803  noetalem1  27804  conway  27862  madebdayim  27944  madebdaylemlrcut  27955  negsprop  28085  mulscom  28183  absmuls  28286  remulscl  28452  tgjustf  28499  axsegcon  28960  axeuclidlem  28995  axcontlem9  29005  eengtrkg  29019  cusgrsize2inds  29489  pthdepisspth  29771  usgr2wlkneq  29792  crctcshwlkn0  29854  wpthswwlks2on  29994  clwwlkccatlem  30021  wwlksext2clwwlk  30089  umgr3v3e3cycl  30216  vdgn1frgrv2  30328  frgrwopreglem5  30353  frgrwopreg  30355  frgrhash2wsp  30364  numclwwlk1lem2fo  30390  vacn  30726  smcnlem  30729  0lno  30822  chocunii  31333  occl  31336  5oalem1  31686  3oalem2  31695  unoplin  31952  hmoplin  31974  lnconi  32065  kbass5  32152  mdslmd1lem1  32357  mdslmd1lem2  32358  mdsymlem2  32436  cdj1i  32465  opreu2reuALT  32505  unidifsnne  32564  disjabrex  32604  disjabrexf  32605  acunirnmpt  32677  fgreu  32690  suppovss  32697  xrge0infss  32767  xrofsup  32774  fsumiunle  32833  mgcf1o  32976  xrge0addgt0  33003  submomnd  33060  fzto1st1  33095  cyc3genpm  33145  cycpmgcl  33146  submarchi  33166  archiabllem1  33173  archiabllem2a  33174  rlocval  33231  isarchiofld  33312  imaslmod  33346  lindfpropd  33375  unitprodclb  33382  elrspunidl  33421  dfufd2lem  33542  lvecdim0  33619  constrmon  33734  locfinreflem  33786  zarcmplem  33827  rge0scvg  33895  lmxrge0  33898  lmdvg  33899  qqhval2  33928  esumrnmpt2  34032  esumfsup  34034  esumpcvgval  34042  esumcvg  34050  esumgect  34054  esumiun  34058  sigaclfu2  34085  sigainb  34100  insiga  34101  fiunelros  34138  measinblem  34184  measinb  34185  measdivcst  34188  measdivcstALTV  34189  omssubadd  34265  oddpwdc  34319  dstrvprob  34436  sgnmul  34507  sgnsub  34509  signsply0  34528  signstfvneq0  34549  bnj1408  35012  ptpconn  35201  sconnpi1  35207  resconn  35214  cvmliftmolem2  35250  cvmlift2lem12  35282  satfsschain  35332  satffunlem2lem1  35372  ifscgr  36008  cgrxfr  36019  outsideofeu  36095  linethru  36117  neibastop1  36325  dnicn  36458  irrdifflemf  37291  irrdiff  37292  fin2so  37567  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem28  37608  poimirlem31  37611  mblfinlem2  37618  mblfinlem3  37619  itg2addnclem  37631  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  ssbnd  37748  totbndbnd  37749  prtlem10  38821  lssats  38968  lkrlss  39051  lshpset2N  39075  2dim  39427  islvol5  39536  paddasslem11  39787  pexmidlem8N  39934  ltrnid  40092  idltrn  40107  trlator0  40128  trlnidatb  40134  cdlemf2  40519  cdlemg2cex  40548  tendodi1  40741  tendodi2  40742  diblss  41127  dihopelvalcpre  41205  dih1dimatlem  41286  dihglblem6  41297  primrootscoprmpow  42056  posbezout  42057  aks6d1c4  42081  sticksstones22  42125  aks6d1c6isolem1  42131  aks6d1c6isolem2  42132  aks6d1c6lem5  42134  grpods  42151  unitscyglem3  42154  unitscyglem4  42155  remul01  42383  sn-subeu  42402  sn-0tie0  42415  sn-itrere  42444  sn-retire  42445  prjspertr  42560  prjspersym  42562  0prjspnrel  42582  mzpsubst  42704  mzpcompact2lem  42707  eldioph2  42718  eldioph2b  42719  diophren  42769  pell14qrexpcl  42823  elpell1qr2  42828  monotoddzzfi  42899  acongtr  42935  acongrep  42937  jm2.19lem4  42949  jm2.26a  42957  jm2.26lem3  42958  jm2.26  42959  isnumbasgrplem2  43061  mendassa  43151  omord2lim  43262  cantnftermord  43282  tfsconcatfv1  43301  tfsconcatfv2  43302  naddcnffo  43326  naddcnfcom  43328  naddcnfid1  43329  naddgeoa  43356  clsk3nimkb  44002  prmunb2  44280  4an4132  44470  fiiuncl  44967  ssinc  44989  ssdec  44990  supxrgelem  45252  infxr  45282  cvgcaule  45407  mullimc  45537  mullimcf  45544  neglimc  45568  climleltrp  45597  climisp  45667  limsupresxr  45687  liminfresxr  45688  liminflimsupclim  45728  xlimliminflimsup  45783  icccncfext  45808  cncfiooicclem1  45814  fprodcncf  45821  dvnprodlem3  45869  iblcncfioo  45899  itgspltprt  45900  stoweidlem7  45928  stoweidlem28  45949  stoweidlem34  45955  stoweidlem48  45969  stoweidlem52  45973  wallispilem3  45988  fourierdlem12  46040  fourierdlem38  46066  fourierdlem39  46067  fourierdlem42  46070  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem51  46078  fourierdlem65  46092  fourierdlem73  46100  fourierdlem76  46103  fourierdlem87  46114  fourierdlem103  46130  fourierdlem104  46131  sge0f1o  46303  sge0le  46328  sge0reuz  46368  ismeannd  46388  isomenndlem  46451  hoicvr  46469  hoidmvle  46521  smflimlem2  46693  smflimmpt  46731  fsupdm  46763  finfdm  46767  imasetpreimafvbijlemf1  47278  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbnd  47683  rrxlinec  48470  iccdisj  48578  fullthinc  48713