Theorem simplll 773

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  f1imass  7022  oeeui  8228  oaabs2  8272  omxpenlem  8618  acndom2  9480  infpwfien  9488  sornom  9699  isf32lem2  9776  isf32lem4  9778  fin1a2lem11  9832  pwfseq  10086  gchina  10121  inttsk  10196  inar1  10197  prlem936  10469  mulcmpblnr  10493  00id  10815  mul02lem1  10816  addid1  10820  cnegex  10821  negeu  10876  add20  11152  ltmul12a  11496  lediv12a  11533  fiminreOLD  11590  cru  11630  qextltlem  12596  xmullem  12658  xlemul1a  12682  ixxss12  12759  ioodisj  12869  elfz0fzfz0  13013  fsuppmapnn0fz  13365  seqf1o  13412  mulexpz  13470  leexp1a  13540  seqcoll  13823  swrdswrdlem  14066  pfxccatin12lem3  14094  abs3lem  14698  cau3lem  14714  climcau  15027  sumeq2ii  15050  climcndslem1  15204  climcndslem2  15205  geomulcvg  15232  mertenslem1  15240  mertenslem2  15241  mertens  15242  prodeq2ii  15267  prodmolem2  15289  bitsfzo  15784  sadadd2lem2  15799  dvdsmulgcd  15905  qredeu  16002  pc2dvds  16215  pcz  16217  ramcl  16365  firest  16706  mreexexlemd  16915  isacs2  16924  iscatd2  16952  ipodrsima  17775  mrelatlub  17796  mndpropd  17936  mhmeql  17990  mhmid  18220  mhmmnd  18221  issubg4  18298  cycsubm  18345  cycsubmcom  18347  gasubg  18432  symgextf  18545  pmtr3ncom  18603  gexdvds  18709  oddvdssubg  18975  cyggeninv  19002  cyggenod  19003  issrg  19257  dvdsrmul1  19403  unitgrp  19417  cntzsubr  19568  islmhm2  19810  lmhmeql  19827  lbspropd  19871  lssacsex  19916  issubassa2  20121  mplbas2  20251  psgndiflemA  20745  isphl  20772  ocvocv  20815  lindfmm  20971  scmatmats  21120  smatvscl  21133  mdetdiag  21208  m2cpmfo  21364  pmatcollpw3fi1lem1  21394  pm2mpf1  21407  pm2mpghm  21424  fvmptnn04if  21457  chfacfscmulfsupp  21467  chfacfpmmulfsupp  21471  neissex  21735  neiptoptop  21739  neiptopnei  21740  restbas  21766  tgrest  21767  restopnb  21783  cnpco  21875  isreg2  21985  iunconn  22036  1stcrest  22061  2ndcctbss  22063  2ndcomap  22066  2ndcsep  22067  dislly  22105  kgencn2  22165  ptbasfi  22189  txhaus  22255  txkgen  22260  txconn  22297  qtopcn  22322  regr1lem2  22348  kqnrmlem1  22351  kqnrmlem2  22352  trfbas2  22451  trfil2  22495  flimcf  22590  hauspwpwf1  22595  fclscf  22633  flimfnfcls  22636  ustexsym  22824  ustuqtop4  22853  utop3cls  22860  utopreg  22861  ucnima  22890  ucncn  22894  metequiv2  23120  prdsxmslem2  23139  metcnpi3  23156  metustto  23163  metustid  23164  metustexhalf  23166  ngptgp  23245  xrsblre  23419  icccmp  23433  reconnlem1  23434  reconn  23436  opnreen  23439  metdsf  23456  metdscn  23464  fsumcn  23478  elcncf2  23498  cncfmet  23516  pcoass  23628  lmcau  23916  rrxdstprj1  24012  pmltpc  24051  ivthlem2  24053  ivthlem3  24054  ovollb2  24090  volsup  24157  ioombl1  24163  ioorf  24174  dyadss  24195  dyaddisjlem  24196  dyadmax  24199  volcn  24207  cncombf  24259  mbflimsup  24267  itg2const2  24342  iblss2  24406  cpnord  24532  dvmptfsum  24572  fta1g  24761  plydivex  24886  fta1  24897  aannenlem1  24917  ulmdvlem3  24990  advlogexp  25238  cxpmul2z  25274  atantayl2  25516  jensen  25566  isppw2  25692  lgsqr  25927  lgsqrmodndvds  25929  lgsdchrval  25930  lgsquad3  25963  2sqb  26008  dchrisumlem3  26067  pntrsumbnd2  26143  tgjustf  26259  axsegcon  26713  axeuclidlem  26748  axcontlem9  26758  eengtrkg  26772  cusgrsize2inds  27235  pthdepisspth  27516  usgr2wlkneq  27537  crctcshwlkn0  27599  wpthswwlks2on  27740  clwwlkccatlem  27767  wwlksext2clwwlk  27836  umgr3v3e3cycl  27963  vdgn1frgrv2  28075  frgrwopreglem5  28100  frgrwopreg  28102  frgrhash2wsp  28111  numclwwlk1lem2fo  28137  vacn  28471  smcnlem  28474  0lno  28567  chocunii  29078  occl  29081  5oalem1  29431  3oalem2  29440  unoplin  29697  hmoplin  29719  lnconi  29810  kbass5  29897  mdslmd1lem1  30102  mdslmd1lem2  30103  mdsymlem2  30181  cdj1i  30210  opreu2reuALT  30240  unidifsnne  30296  disjabrex  30332  disjabrexf  30333  acunirnmpt  30404  fgreu  30417  suppovss  30426  xrge0infss  30484  xrofsup  30492  fsumiunle  30545  xrge0addgt0  30678  submomnd  30711  fzto1st1  30744  cyc3genpm  30794  cycpmgcl  30795  submarchi  30815  archiabllem1  30822  archiabllem2a  30823  isarchiofld  30890  imaslmod  30922  lindfpropd  30942  lvecdim0  31005  locfinreflem  31104  rge0scvg  31192  lmxrge0  31195  lmdvg  31196  qqhval2  31223  esumrnmpt2  31327  esumfsup  31329  esumpcvgval  31337  esumcvg  31345  esumgect  31349  esumiun  31353  sigaclfu2  31380  sigainb  31395  insiga  31396  fiunelros  31433  measinblem  31479  measinb  31480  measdivcst  31483  measdivcstALTV  31484  omssubadd  31558  oddpwdc  31612  dstrvprob  31729  sgnmul  31800  sgnsub  31802  signsply0  31821  signstfvneq0  31842  bnj1408  32308  ptpconn  32480  sconnpi1  32486  resconn  32493  cvmliftmolem2  32529  cvmlift2lem12  32561  satfsschain  32611  satffunlem2lem1  32651  poseq  33095  noetalem3  33219  noetalem5  33221  conway  33264  ifscgr  33505  cgrxfr  33516  outsideofeu  33592  linethru  33614  neibastop1  33707  dnicn  33831  fin2so  34894  matunitlindflem1  34903  matunitlindflem2  34904  poimirlem28  34935  poimirlem31  34938  mblfinlem2  34945  mblfinlem3  34946  itg2addnclem  34958  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  ssbnd  35081  totbndbnd  35082  prtlem10  36016  lssats  36163  lkrlss  36246  lshpset2N  36270  2dim  36621  islvol5  36730  paddasslem11  36981  pexmidlem8N  37128  ltrnid  37286  idltrn  37301  trlator0  37322  trlnidatb  37328  cdlemf2  37713  cdlemg2cex  37742  tendodi1  37935  tendodi2  37936  diblss  38321  dihopelvalcpre  38399  dih1dimatlem  38480  dihglblem6  38491  remul01  39257  prjspertr  39275  prjspersym  39277  0prjspnrel  39289  mzpsubst  39365  mzpcompact2lem  39368  eldioph2  39379  eldioph2b  39380  diophren  39430  pell14qrexpcl  39484  elpell1qr2  39489  monotoddzzfi  39559  acongtr  39595  acongrep  39597  jm2.19lem4  39609  jm2.26a  39617  jm2.26lem3  39618  jm2.26  39619  isnumbasgrplem2  39724  mendassa  39814  clsk3nimkb  40410  prmunb2  40663  4an4132  40853  fiiuncl  41347  ssinc  41373  ssdec  41374  supxrgelem  41625  infxr  41655  mullimc  41917  mullimcf  41924  neglimc  41948  climleltrp  41977  climisp  42047  limsupresxr  42067  liminfresxr  42068  liminflimsupclim  42108  xlimliminflimsup  42163  icccncfext  42190  cncfiooicclem1  42196  fprodcncf  42204  dvnprodlem3  42253  iblcncfioo  42283  itgspltprt  42284  stoweidlem7  42312  stoweidlem28  42333  stoweidlem34  42339  stoweidlem48  42353  stoweidlem52  42357  wallispilem3  42372  fourierdlem12  42424  fourierdlem38  42450  fourierdlem39  42451  fourierdlem42  42454  fourierdlem46  42457  fourierdlem48  42459  fourierdlem49  42460  fourierdlem50  42461  fourierdlem51  42462  fourierdlem65  42476  fourierdlem73  42484  fourierdlem76  42487  fourierdlem87  42498  fourierdlem103  42514  fourierdlem104  42515  sge0f1o  42684  sge0le  42709  sge0reuz  42749  ismeannd  42769  isomenndlem  42832  hoicvr  42850  hoidmvle  42902  smflimlem2  43068  smflimmpt  43104  imasetpreimafvbijlemf1  43584  nnsum4primeseven  43985  nnsum4primesevenALTV  43986  bgoldbtbndlem2  43991  bgoldbtbndlem3  43992  bgoldbtbnd  43994  isomuspgrlem2  44018  mgmhmeql  44090  rrxlinec  44743