Theorem simplll 784

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 740	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 209  df-an 400

This theorem is referenced by:  f1imass  7242  poseq  8131  oeeui  8565  oaabs2  8612  naddssim  8649  omxpenlem  9043  findcard3  9220  wemappo  9490  acndom2  10003  infpwfien  10011  sornom  10227  isf32lem2  10304  isf32lem4  10306  fin1a2lem11  10360  pwfseq  10615  gchina  10650  inttsk  10725  inar1  10726  prlem936  10998  mulcmpblnr  11022  00id  11351  mul02lem1  11352  addrid  11356  cnegex  11357  negeu  11413  add20  11692  ltmul12a  12040  lediv12a  12078  cru  12180  qextltlem  13198  xmullem  13260  xlemul1a  13284  ixxss12  13362  ioodisj  13479  elfz0fzfz0  13631  fsuppmapnn0fz  14002  seqf1o  14049  mulexpz  14108  leexp1a  14181  seqcoll  14470  swrdswrdlem  14710  pfxccatin12lem3  14738  sgnsub  15109  sgnmul  15110  abs3lem  15356  cau3lem  15372  climcau  15688  sumeq2ii  15710  climcndslem1  15869  climcndslem2  15870  geomulcvg  15896  mertenslem1  15904  mertenslem2  15905  mertens  15906  prodeq2ii  15931  prodmolem2  15955  bitsfzo  16459  sadadd2lem2  16474  dvdsmulgcd  16580  qredeu  16682  pc2dvds  16905  pcz  16907  ramcl  17055  firest  17451  mreexexlemd  17666  isacs2  17675  iscatd2  17703  ipodrsima  18563  mrelatlub  18584  mgmhmeql  18740  sgrppropd  18755  mndpropd  18783  mhmeql  18850  mhmid  19095  mhmmnd  19096  issubg4  19177  cycsubm  19233  cycsubmcom  19235  gasubg  19332  symgextf  19447  pmtr3ncom  19505  gexdvds  19614  oddvdssubg  19885  imasabl  19906  cyggeninv  19913  cyggenod  19914  submomnd  20162  issrg  20224  dvdsrmul1  20404  unitgrp  20418  cntzsubrng  20603  cntzsubr  20642  islmhm2  21092  lmhmeql  21109  lbspropd  21153  lssacsex  21201  rngqiprngimfo  21358  psgndiflemA  21640  isphl  21667  ocvocv  21710  lindfmm  21866  issubassa2  21931  mplbas2  22082  scmatmats  22558  smatvscl  22571  mdetdiag  22646  m2cpmfo  22803  pmatcollpw3fi1lem1  22833  pm2mpf1  22846  pm2mpghm  22863  fvmptnn04if  22896  chfacfscmulfsupp  22906  chfacfpmmulfsupp  22910  neissex  23174  neiptoptop  23178  neiptopnei  23179  restbas  23205  tgrest  23206  restopnb  23222  cnpco  23314  isreg2  23424  iunconn  23475  1stcrest  23500  2ndcctbss  23502  2ndcomap  23505  2ndcsep  23506  dislly  23544  kgencn2  23604  ptbasfi  23628  txhaus  23694  txkgen  23699  txconn  23736  qtopcn  23761  regr1lem2  23787  kqnrmlem1  23790  kqnrmlem2  23791  trfbas2  23890  trfil2  23934  flimcf  24029  hauspwpwf1  24034  fclscf  24072  flimfnfcls  24075  ustexsym  24263  ustuqtop4  24291  utop3cls  24298  utopreg  24299  ucnima  24327  ucncn  24331  metequiv2  24557  prdsxmslem2  24576  metcnpi3  24593  metustto  24600  metustid  24601  metustexhalf  24603  ngptgp  24683  xrsblre  24859  icccmp  24873  reconnlem1  24874  reconn  24876  opnreen  24879  metdsf  24896  metdscn  24904  mpomulcn  24916  fsumcn  24919  elcncf2  24939  cncfmet  24958  pcoass  25073  lmcau  25362  rrxdstprj1  25458  pmltpc  25499  ivthlem2  25501  ivthlem3  25502  ovollb2  25538  volsup  25605  ioombl1  25611  ioorf  25622  dyadss  25643  dyaddisjlem  25644  dyadmax  25647  volcn  25655  cncombf  25707  mbflimsup  25715  itg2const2  25790  iblss2  25855  cpnord  25984  dvmptfsum  26024  fta1g  26217  plydivex  26348  fta1  26359  aannenlem1  26379  ulmdvlem3  26452  advlogexp  26707  cxpmul2z  26743  atantayl2  26990  jensen  27040  isppw2  27166  lgsqr  27402  lgsqrmodndvds  27404  lgsdchrval  27405  lgsquad3  27438  2sqb  27483  dchrisumlem3  27542  pntrsumbnd2  27618  noinfbnd1lem5  27778  noetasuplem4  27787  noetainflem4  27791  noetalem1  27792  conway  27859  eqcuts3  27884  madebdayim  27968  madebdaylemlrcut  27979  negsprop  28115  mulscom  28219  absmuls  28324  bdayons  28356  addonbday  28359  bdayfinbndlem1  28547  remulscl  28582  tgjustf  28629  axsegcon  29084  axeuclidlem  29119  axcontlem9  29129  eengtrkg  29143  cusgrsize2inds  29610  pthdepisspth  29891  usgr2wlkneq  29912  crctcshwlkn0  29977  wpthswwlks2on  30120  clwwlkccatlem  30147  wwlksext2clwwlk  30215  umgr3v3e3cycl  30342  vdgn1frgrv2  30454  frgrwopreglem5  30479  frgrwopreg  30481  frgrhash2wsp  30490  numclwwlk1lem2fo  30516  vacn  30853  smcnlem  30856  0lno  30949  chocunii  31460  occl  31463  5oalem1  31813  3oalem2  31822  unoplin  32079  hmoplin  32101  lnconi  32192  kbass5  32279  mdslmd1lem1  32484  mdslmd1lem2  32485  mdsymlem2  32563  cdj1i  32592  opreu2reuALT  32634  unidifsnne  32694  disjabrex  32741  disjabrexf  32742  acunirnmpt  32821  fgreu  32833  suppovss  32843  xrge0infss  32922  xrofsup  32929  fsumiunle  32991  mgcf1o  33141  xrge0addgt0  33155  fzto1st1  33242  cyc3genpm  33292  cycpmgcl  33293  submarchi  33326  archiabllem1  33333  archiabllem2a  33334  isarchiofld  33339  rlocval  33400  imaslmod  33499  lindfpropd  33528  unitprodclb  33535  elrspunidl  33574  drnglring  33648  dflring3  33653  dfufd2lem  33705  mplmulmvr  33796  lvecdim0  33864  constrmon  34001  constrextdg2  34006  locfinreflem  34097  zarcmplem  34138  rge0scvg  34206  lmxrge0  34209  lmdvg  34210  qqhval2  34239  esumrnmpt2  34325  esumfsup  34327  esumpcvgval  34335  esumcvg  34343  esumgect  34347  esumiun  34351  sigaclfu2  34378  sigainb  34393  insiga  34394  fiunelros  34431  measinblem  34477  measinb  34478  measdivcst  34481  measdivcstALTV  34482  omssubadd  34557  oddpwdc  34611  dstrvprob  34729  signsply0  34805  signstfvneq0  34826  bnj1408  35291  ptpconn  35543  sconnpi1  35549  resconn  35556  cvmliftmolem2  35592  cvmlift2lem12  35624  satfsschain  35674  satffunlem2lem1  35714  ifscgr  36354  cgrxfr  36365  outsideofeu  36441  linethru  36463  nmulcom  36504  neibastop1  36679  dnicn  36890  irrdifflemf  37777  irrdiff  37778  fin2so  38066  matunitlindflem1  38075  matunitlindflem2  38076  poimirlem28  38107  poimirlem31  38110  mblfinlem2  38117  mblfinlem3  38118  itg2addnclem  38130  ftc1anclem7  38158  ftc1anclem8  38159  ftc1anc  38160  ssbnd  38247  totbndbnd  38248  prtlem10  39449  lssats  39596  lkrlss  39679  lshpset2N  39703  2dim  40054  islvol5  40163  paddasslem11  40414  pexmidlem8N  40561  ltrnid  40719  idltrn  40734  trlator0  40755  trlnidatb  40761  cdlemf2  41146  cdlemg2cex  41175  tendodi1  41368  tendodi2  41369  diblss  41754  dihopelvalcpre  41832  dih1dimatlem  41913  dihglblem6  41924  primrootscoprmpow  42676  posbezout  42677  aks6d1c4  42701  sticksstones22  42745  aks6d1c6isolem1  42751  aks6d1c6isolem2  42752  aks6d1c6lem5  42754  grpods  42771  unitscyglem3  42774  unitscyglem4  42775  remul01  42976  sn-subeu  42996  sn-0tie0  43033  prjspertr  43147  prjspersym  43149  0prjspnrel  43169  mzpsubst  43289  mzpcompact2lem  43292  eldioph2  43303  eldioph2b  43304  diophren  43350  pell14qrexpcl  43404  elpell1qr2  43409  monotoddzzfi  43479  acongtr  43515  acongrep  43517  jm2.19lem4  43529  jm2.26a  43537  jm2.26lem3  43538  jm2.26  43539  isnumbasgrplem2  43641  mendassa  43727  omord2lim  43837  cantnftermord  43857  tfsconcatfv1  43876  tfsconcatfv2  43877  naddcnffo  43901  naddcnfcom  43903  naddcnfid1  43904  naddgeoa  43931  clsk3nimkb  44576  prmunb2  44847  4an4132  45035  fiiuncl  45605  ssinc  45625  ssdec  45626  supxrgelem  45873  infxr  45902  cvgcaule  46025  mullimc  46152  mullimcf  46159  neglimc  46181  climleltrp  46210  climisp  46280  limsupresxr  46300  liminfresxr  46301  liminflimsupclim  46341  xlimliminflimsup  46396  icccncfext  46421  cncfiooicclem1  46427  fprodcncf  46434  dvnprodlem3  46482  iblcncfioo  46512  itgspltprt  46513  stoweidlem7  46541  stoweidlem28  46562  stoweidlem34  46568  stoweidlem48  46582  stoweidlem52  46586  wallispilem3  46601  fourierdlem12  46653  fourierdlem38  46679  fourierdlem39  46680  fourierdlem42  46683  fourierdlem46  46686  fourierdlem48  46688  fourierdlem49  46689  fourierdlem50  46690  fourierdlem51  46691  fourierdlem65  46705  fourierdlem73  46713  fourierdlem76  46716  fourierdlem87  46727  fourierdlem103  46743  fourierdlem104  46744  sge0f1o  46916  sge0le  46941  sge0reuz  46981  ismeannd  47001  isomenndlem  47064  hoicvr  47082  hoidmvle  47134  smflimlem2  47306  smflimmpt  47344  fsupdm  47376  finfdm  47380  nndivides2  47938  imasetpreimafvbijlemf1  47970  nnsum4primeseven  48382  nnsum4primesevenALTV  48383  bgoldbtbndlem2  48388  bgoldbtbndlem3  48389  bgoldbtbnd  48391  isubgr3stgrlem6  48553  rrxlinec  49318  iccdisj  49479  upfval  49757  fullthinc  50031