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 399

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 210  df-an 400

This theorem is referenced by:  f1imass  7000  oeeui  8211  oaabs2  8255  omxpenlem  8601  acndom2  9465  infpwfien  9473  sornom  9688  isf32lem2  9765  isf32lem4  9767  fin1a2lem11  9821  pwfseq  10075  gchina  10110  inttsk  10185  inar1  10186  prlem936  10458  mulcmpblnr  10482  00id  10804  mul02lem1  10805  addid1  10809  cnegex  10810  negeu  10865  add20  11141  ltmul12a  11485  lediv12a  11522  cru  11617  qextltlem  12583  xmullem  12645  xlemul1a  12669  ixxss12  12746  ioodisj  12860  elfz0fzfz0  13007  fsuppmapnn0fz  13359  seqf1o  13407  mulexpz  13465  leexp1a  13535  seqcoll  13818  swrdswrdlem  14057  pfxccatin12lem3  14085  abs3lem  14690  cau3lem  14706  climcau  15019  sumeq2ii  15042  climcndslem1  15196  climcndslem2  15197  geomulcvg  15224  mertenslem1  15232  mertenslem2  15233  mertens  15234  prodeq2ii  15259  prodmolem2  15281  bitsfzo  15774  sadadd2lem2  15789  dvdsmulgcd  15895  qredeu  15992  pc2dvds  16205  pcz  16207  ramcl  16355  firest  16698  mreexexlemd  16907  isacs2  16916  iscatd2  16944  ipodrsima  17767  mrelatlub  17788  mndpropd  17928  mhmeql  17982  mhmid  18212  mhmmnd  18213  issubg4  18290  cycsubm  18337  cycsubmcom  18339  gasubg  18424  symgextf  18537  pmtr3ncom  18595  gexdvds  18701  oddvdssubg  18968  cyggeninv  18995  cyggenod  18996  issrg  19250  dvdsrmul1  19399  unitgrp  19413  cntzsubr  19561  islmhm2  19803  lmhmeql  19820  lbspropd  19864  lssacsex  19909  psgndiflemA  20290  isphl  20317  ocvocv  20360  lindfmm  20516  issubassa2  20578  mplbas2  20710  scmatmats  21116  smatvscl  21129  mdetdiag  21204  m2cpmfo  21361  pmatcollpw3fi1lem1  21391  pm2mpf1  21404  pm2mpghm  21421  fvmptnn04if  21454  chfacfscmulfsupp  21464  chfacfpmmulfsupp  21468  neissex  21732  neiptoptop  21736  neiptopnei  21737  restbas  21763  tgrest  21764  restopnb  21780  cnpco  21872  isreg2  21982  iunconn  22033  1stcrest  22058  2ndcctbss  22060  2ndcomap  22063  2ndcsep  22064  dislly  22102  kgencn2  22162  ptbasfi  22186  txhaus  22252  txkgen  22257  txconn  22294  qtopcn  22319  regr1lem2  22345  kqnrmlem1  22348  kqnrmlem2  22349  trfbas2  22448  trfil2  22492  flimcf  22587  hauspwpwf1  22592  fclscf  22630  flimfnfcls  22633  ustexsym  22821  ustuqtop4  22850  utop3cls  22857  utopreg  22858  ucnima  22887  ucncn  22891  metequiv2  23117  prdsxmslem2  23136  metcnpi3  23153  metustto  23160  metustid  23161  metustexhalf  23163  ngptgp  23242  xrsblre  23416  icccmp  23430  reconnlem1  23431  reconn  23433  opnreen  23436  metdsf  23453  metdscn  23461  fsumcn  23475  elcncf2  23495  cncfmet  23514  pcoass  23629  lmcau  23917  rrxdstprj1  24013  pmltpc  24054  ivthlem2  24056  ivthlem3  24057  ovollb2  24093  volsup  24160  ioombl1  24166  ioorf  24177  dyadss  24198  dyaddisjlem  24199  dyadmax  24202  volcn  24210  cncombf  24262  mbflimsup  24270  itg2const2  24345  iblss2  24409  cpnord  24538  dvmptfsum  24578  fta1g  24768  plydivex  24893  fta1  24904  aannenlem1  24924  ulmdvlem3  24997  advlogexp  25246  cxpmul2z  25282  atantayl2  25524  jensen  25574  isppw2  25700  lgsqr  25935  lgsqrmodndvds  25937  lgsdchrval  25938  lgsquad3  25971  2sqb  26016  dchrisumlem3  26075  pntrsumbnd2  26151  tgjustf  26267  axsegcon  26721  axeuclidlem  26756  axcontlem9  26766  eengtrkg  26780  cusgrsize2inds  27243  pthdepisspth  27524  usgr2wlkneq  27545  crctcshwlkn0  27607  wpthswwlks2on  27747  clwwlkccatlem  27774  wwlksext2clwwlk  27842  umgr3v3e3cycl  27969  vdgn1frgrv2  28081  frgrwopreglem5  28106  frgrwopreg  28108  frgrhash2wsp  28117  numclwwlk1lem2fo  28143  vacn  28477  smcnlem  28480  0lno  28573  chocunii  29084  occl  29087  5oalem1  29437  3oalem2  29446  unoplin  29703  hmoplin  29725  lnconi  29816  kbass5  29903  mdslmd1lem1  30108  mdslmd1lem2  30109  mdsymlem2  30187  cdj1i  30216  opreu2reuALT  30247  unidifsnne  30308  disjabrex  30345  disjabrexf  30346  acunirnmpt  30422  fgreu  30435  suppovss  30443  xrge0infss  30510  xrofsup  30518  fsumiunle  30571  xrge0addgt0  30725  submomnd  30761  fzto1st1  30794  cyc3genpm  30844  cycpmgcl  30845  submarchi  30865  archiabllem1  30872  archiabllem2a  30873  isarchiofld  30941  imaslmod  30973  lindfpropd  30996  elrspunidl  31014  lvecdim0  31093  locfinreflem  31193  zarcmplem  31234  rge0scvg  31302  lmxrge0  31305  lmdvg  31306  qqhval2  31333  esumrnmpt2  31437  esumfsup  31439  esumpcvgval  31447  esumcvg  31455  esumgect  31459  esumiun  31463  sigaclfu2  31490  sigainb  31505  insiga  31506  fiunelros  31543  measinblem  31589  measinb  31590  measdivcst  31593  measdivcstALTV  31594  omssubadd  31668  oddpwdc  31722  dstrvprob  31839  sgnmul  31910  sgnsub  31912  signsply0  31931  signstfvneq0  31952  bnj1408  32418  ptpconn  32593  sconnpi1  32599  resconn  32606  cvmliftmolem2  32642  cvmlift2lem12  32674  satfsschain  32724  satffunlem2lem1  32764  poseq  33208  noetalem3  33332  noetalem5  33334  conway  33377  ifscgr  33618  cgrxfr  33629  outsideofeu  33705  linethru  33727  neibastop1  33820  dnicn  33944  irrdifflemf  34739  irrdiff  34740  fin2so  35044  matunitlindflem1  35053  matunitlindflem2  35054  poimirlem28  35085  poimirlem31  35088  mblfinlem2  35095  mblfinlem3  35096  itg2addnclem  35108  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  ssbnd  35226  totbndbnd  35227  prtlem10  36161  lssats  36308  lkrlss  36391  lshpset2N  36415  2dim  36766  islvol5  36875  paddasslem11  37126  pexmidlem8N  37273  ltrnid  37431  idltrn  37446  trlator0  37467  trlnidatb  37473  cdlemf2  37858  cdlemg2cex  37887  tendodi1  38080  tendodi2  38081  diblss  38466  dihopelvalcpre  38544  dih1dimatlem  38625  dihglblem6  38636  remul01  39545  sn-subeu  39563  sn-0tie0  39576  itrere  39591  retire  39592  prjspertr  39599  prjspersym  39601  0prjspnrel  39613  mzpsubst  39689  mzpcompact2lem  39692  eldioph2  39703  eldioph2b  39704  diophren  39754  pell14qrexpcl  39808  elpell1qr2  39813  monotoddzzfi  39883  acongtr  39919  acongrep  39921  jm2.19lem4  39933  jm2.26a  39941  jm2.26lem3  39942  jm2.26  39943  isnumbasgrplem2  40048  mendassa  40138  clsk3nimkb  40743  prmunb2  41015  4an4132  41205  fiiuncl  41699  ssinc  41723  ssdec  41724  supxrgelem  41969  infxr  41999  mullimc  42258  mullimcf  42265  neglimc  42289  climleltrp  42318  climisp  42388  limsupresxr  42408  liminfresxr  42409  liminflimsupclim  42449  xlimliminflimsup  42504  icccncfext  42529  cncfiooicclem1  42535  fprodcncf  42542  dvnprodlem3  42590  iblcncfioo  42620  itgspltprt  42621  stoweidlem7  42649  stoweidlem28  42670  stoweidlem34  42676  stoweidlem48  42690  stoweidlem52  42694  wallispilem3  42709  fourierdlem12  42761  fourierdlem38  42787  fourierdlem39  42788  fourierdlem42  42791  fourierdlem46  42794  fourierdlem48  42796  fourierdlem49  42797  fourierdlem50  42798  fourierdlem51  42799  fourierdlem65  42813  fourierdlem73  42821  fourierdlem76  42824  fourierdlem87  42835  fourierdlem103  42851  fourierdlem104  42852  sge0f1o  43021  sge0le  43046  sge0reuz  43086  ismeannd  43106  isomenndlem  43169  hoicvr  43187  hoidmvle  43239  smflimlem2  43405  smflimmpt  43441  imasetpreimafvbijlemf1  43921  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  bgoldbtbndlem2  44324  bgoldbtbndlem3  44325  bgoldbtbnd  44327  isomuspgrlem2  44351  mgmhmeql  44423  rrxlinec  45150