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 397

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 206  df-an 398

This theorem is referenced by:  f1imass  7263  poseq  8144  oeeui  8602  oaabs2  8648  naddssim  8684  omxpenlem  9073  findcard3  9285  wemappo  9544  acndom2  10049  infpwfien  10057  sornom  10272  isf32lem2  10349  isf32lem4  10351  fin1a2lem11  10405  pwfseq  10659  gchina  10694  inttsk  10769  inar1  10770  prlem936  11042  mulcmpblnr  11066  00id  11389  mul02lem1  11390  addrid  11394  cnegex  11395  negeu  11450  add20  11726  ltmul12a  12070  lediv12a  12107  cru  12204  qextltlem  13181  xmullem  13243  xlemul1a  13267  ixxss12  13344  ioodisj  13459  elfz0fzfz0  13606  fsuppmapnn0fz  13961  seqf1o  14009  mulexpz  14068  leexp1a  14140  seqcoll  14425  swrdswrdlem  14654  pfxccatin12lem3  14682  abs3lem  15285  cau3lem  15301  climcau  15617  sumeq2ii  15639  climcndslem1  15795  climcndslem2  15796  geomulcvg  15822  mertenslem1  15830  mertenslem2  15831  mertens  15832  prodeq2ii  15857  prodmolem2  15879  bitsfzo  16376  sadadd2lem2  16391  dvdsmulgcd  16497  qredeu  16595  pc2dvds  16812  pcz  16814  ramcl  16962  firest  17378  mreexexlemd  17588  isacs2  17597  iscatd2  17625  ipodrsima  18494  mrelatlub  18515  sgrppropd  18622  mndpropd  18650  mhmeql  18707  mhmid  18946  mhmmnd  18947  issubg4  19025  cycsubm  19079  cycsubmcom  19081  gasubg  19166  symgextf  19285  pmtr3ncom  19343  gexdvds  19452  oddvdssubg  19723  imasabl  19744  cyggeninv  19751  cyggenod  19752  issrg  20011  dvdsrmul1  20183  unitgrp  20197  cntzsubr  20353  islmhm2  20649  lmhmeql  20666  lbspropd  20710  lssacsex  20757  psgndiflemA  21154  isphl  21181  ocvocv  21224  lindfmm  21382  issubassa2  21446  mplbas2  21597  scmatmats  22013  smatvscl  22026  mdetdiag  22101  m2cpmfo  22258  pmatcollpw3fi1lem1  22288  pm2mpf1  22301  pm2mpghm  22318  fvmptnn04if  22351  chfacfscmulfsupp  22361  chfacfpmmulfsupp  22365  neissex  22631  neiptoptop  22635  neiptopnei  22636  restbas  22662  tgrest  22663  restopnb  22679  cnpco  22771  isreg2  22881  iunconn  22932  1stcrest  22957  2ndcctbss  22959  2ndcomap  22962  2ndcsep  22963  dislly  23001  kgencn2  23061  ptbasfi  23085  txhaus  23151  txkgen  23156  txconn  23193  qtopcn  23218  regr1lem2  23244  kqnrmlem1  23247  kqnrmlem2  23248  trfbas2  23347  trfil2  23391  flimcf  23486  hauspwpwf1  23491  fclscf  23529  flimfnfcls  23532  ustexsym  23720  ustuqtop4  23749  utop3cls  23756  utopreg  23757  ucnima  23786  ucncn  23790  metequiv2  24019  prdsxmslem2  24038  metcnpi3  24055  metustto  24062  metustid  24063  metustexhalf  24065  ngptgp  24145  xrsblre  24327  icccmp  24341  reconnlem1  24342  reconn  24344  opnreen  24347  metdsf  24364  metdscn  24372  fsumcn  24386  elcncf2  24406  cncfmet  24425  pcoass  24540  lmcau  24830  rrxdstprj1  24926  pmltpc  24967  ivthlem2  24969  ivthlem3  24970  ovollb2  25006  volsup  25073  ioombl1  25079  ioorf  25090  dyadss  25111  dyaddisjlem  25112  dyadmax  25115  volcn  25123  cncombf  25175  mbflimsup  25183  itg2const2  25259  iblss2  25323  cpnord  25452  dvmptfsum  25492  fta1g  25685  plydivex  25810  fta1  25821  aannenlem1  25841  ulmdvlem3  25914  advlogexp  26163  cxpmul2z  26199  atantayl2  26443  jensen  26493  isppw2  26619  lgsqr  26854  lgsqrmodndvds  26856  lgsdchrval  26857  lgsquad3  26890  2sqb  26935  dchrisumlem3  26994  pntrsumbnd2  27070  noinfbnd1lem5  27230  noetasuplem4  27239  noetainflem4  27243  noetalem1  27244  conway  27300  madebdayim  27382  madebdaylemlrcut  27393  negsprop  27509  mulscom  27595  tgjustf  27724  axsegcon  28185  axeuclidlem  28220  axcontlem9  28230  eengtrkg  28244  cusgrsize2inds  28710  pthdepisspth  28992  usgr2wlkneq  29013  crctcshwlkn0  29075  wpthswwlks2on  29215  clwwlkccatlem  29242  wwlksext2clwwlk  29310  umgr3v3e3cycl  29437  vdgn1frgrv2  29549  frgrwopreglem5  29574  frgrwopreg  29576  frgrhash2wsp  29585  numclwwlk1lem2fo  29611  vacn  29947  smcnlem  29950  0lno  30043  chocunii  30554  occl  30557  5oalem1  30907  3oalem2  30916  unoplin  31173  hmoplin  31195  lnconi  31286  kbass5  31373  mdslmd1lem1  31578  mdslmd1lem2  31579  mdsymlem2  31657  cdj1i  31686  opreu2reuALT  31717  unidifsnne  31773  disjabrex  31813  disjabrexf  31814  acunirnmpt  31884  fgreu  31897  suppovss  31906  xrge0infss  31973  xrofsup  31980  fsumiunle  32035  mgcf1o  32173  xrge0addgt0  32192  submomnd  32228  fzto1st1  32261  cyc3genpm  32311  cycpmgcl  32312  submarchi  32332  archiabllem1  32339  archiabllem2a  32340  isarchiofld  32435  imaslmod  32468  lindfpropd  32498  elrspunidl  32546  lvecdim0  32691  locfinreflem  32820  zarcmplem  32861  rge0scvg  32929  lmxrge0  32932  lmdvg  32933  qqhval2  32962  esumrnmpt2  33066  esumfsup  33068  esumpcvgval  33076  esumcvg  33084  esumgect  33088  esumiun  33092  sigaclfu2  33119  sigainb  33134  insiga  33135  fiunelros  33172  measinblem  33218  measinb  33219  measdivcst  33222  measdivcstALTV  33223  omssubadd  33299  oddpwdc  33353  dstrvprob  33470  sgnmul  33541  sgnsub  33543  signsply0  33562  signstfvneq0  33583  bnj1408  34047  ptpconn  34224  sconnpi1  34230  resconn  34237  cvmliftmolem2  34273  cvmlift2lem12  34305  satfsschain  34355  satffunlem2lem1  34395  ifscgr  35016  cgrxfr  35027  outsideofeu  35103  linethru  35125  mpomulcn  35162  neibastop1  35244  dnicn  35368  irrdifflemf  36206  irrdiff  36207  fin2so  36475  matunitlindflem1  36484  matunitlindflem2  36485  poimirlem28  36516  poimirlem31  36519  mblfinlem2  36526  mblfinlem3  36527  itg2addnclem  36539  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  ssbnd  36656  totbndbnd  36657  prtlem10  37735  lssats  37882  lkrlss  37965  lshpset2N  37989  2dim  38341  islvol5  38450  paddasslem11  38701  pexmidlem8N  38848  ltrnid  39006  idltrn  39021  trlator0  39042  trlnidatb  39048  cdlemf2  39433  cdlemg2cex  39462  tendodi1  39655  tendodi2  39656  diblss  40041  dihopelvalcpre  40119  dih1dimatlem  40200  dihglblem6  40211  sticksstones22  40984  remul01  41280  sn-subeu  41299  sn-0tie0  41312  itrere  41339  retire  41340  prjspertr  41347  prjspersym  41349  0prjspnrel  41369  mzpsubst  41486  mzpcompact2lem  41489  eldioph2  41500  eldioph2b  41501  diophren  41551  pell14qrexpcl  41605  elpell1qr2  41610  monotoddzzfi  41681  acongtr  41717  acongrep  41719  jm2.19lem4  41731  jm2.26a  41739  jm2.26lem3  41740  jm2.26  41741  isnumbasgrplem2  41846  mendassa  41936  omord2lim  42050  cantnftermord  42070  tfsconcatfv1  42089  tfsconcatfv2  42090  naddcnffo  42114  naddcnfcom  42116  naddcnfid1  42117  naddgeoa  42145  clsk3nimkb  42791  prmunb2  43070  4an4132  43260  fiiuncl  43752  ssinc  43776  ssdec  43777  supxrgelem  44047  infxr  44077  cvgcaule  44202  mullimc  44332  mullimcf  44339  neglimc  44363  climleltrp  44392  climisp  44462  limsupresxr  44482  liminfresxr  44483  liminflimsupclim  44523  xlimliminflimsup  44578  icccncfext  44603  cncfiooicclem1  44609  fprodcncf  44616  dvnprodlem3  44664  iblcncfioo  44694  itgspltprt  44695  stoweidlem7  44723  stoweidlem28  44744  stoweidlem34  44750  stoweidlem48  44764  stoweidlem52  44768  wallispilem3  44783  fourierdlem12  44835  fourierdlem38  44861  fourierdlem39  44862  fourierdlem42  44865  fourierdlem46  44868  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem51  44873  fourierdlem65  44887  fourierdlem73  44895  fourierdlem76  44898  fourierdlem87  44909  fourierdlem103  44925  fourierdlem104  44926  sge0f1o  45098  sge0le  45123  sge0reuz  45163  ismeannd  45183  isomenndlem  45246  hoicvr  45264  hoidmvle  45316  smflimlem2  45488  smflimmpt  45526  fsupdm  45558  finfdm  45562  imasetpreimafvbijlemf1  46072  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  bgoldbtbnd  46477  isomuspgrlem2  46501  mgmhmeql  46573  cntzsubrng  46746  rngqiprngimfo  46786  rrxlinec  47422  iccdisj  47531  fullthinc  47666