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 730	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  7198  poseq  8088  oeeui  8517  oaabs2  8564  naddssim  8600  omxpenlem  8991  findcard3  9167  wemappo  9435  acndom2  9945  infpwfien  9953  sornom  10168  isf32lem2  10245  isf32lem4  10247  fin1a2lem11  10301  pwfseq  10555  gchina  10590  inttsk  10665  inar1  10666  prlem936  10938  mulcmpblnr  10962  00id  11288  mul02lem1  11289  addrid  11293  cnegex  11294  negeu  11350  add20  11629  ltmul12a  11977  lediv12a  12015  cru  12117  qextltlem  13101  xmullem  13163  xlemul1a  13187  ixxss12  13265  ioodisj  13382  elfz0fzfz0  13533  fsuppmapnn0fz  13903  seqf1o  13950  mulexpz  14009  leexp1a  14082  seqcoll  14371  swrdswrdlem  14611  pfxccatin12lem3  14639  abs3lem  15246  cau3lem  15262  climcau  15578  sumeq2ii  15600  climcndslem1  15756  climcndslem2  15757  geomulcvg  15783  mertenslem1  15791  mertenslem2  15792  mertens  15793  prodeq2ii  15818  prodmolem2  15842  bitsfzo  16346  sadadd2lem2  16361  dvdsmulgcd  16467  qredeu  16569  pc2dvds  16791  pcz  16793  ramcl  16941  firest  17336  mreexexlemd  17550  isacs2  17559  iscatd2  17587  ipodrsima  18447  mrelatlub  18468  mgmhmeql  18624  sgrppropd  18639  mndpropd  18667  mhmeql  18734  mhmid  18976  mhmmnd  18977  issubg4  19058  cycsubm  19115  cycsubmcom  19117  gasubg  19215  symgextf  19330  pmtr3ncom  19388  gexdvds  19497  oddvdssubg  19768  imasabl  19789  cyggeninv  19796  cyggenod  19797  submomnd  20045  issrg  20107  dvdsrmul1  20288  unitgrp  20302  cntzsubrng  20483  cntzsubr  20522  islmhm2  20973  lmhmeql  20990  lbspropd  21034  lssacsex  21082  rngqiprngimfo  21239  psgndiflemA  21539  isphl  21566  ocvocv  21609  lindfmm  21765  issubassa2  21830  mplbas2  21978  scmatmats  22427  smatvscl  22440  mdetdiag  22515  m2cpmfo  22672  pmatcollpw3fi1lem1  22702  pm2mpf1  22715  pm2mpghm  22732  fvmptnn04if  22765  chfacfscmulfsupp  22775  chfacfpmmulfsupp  22779  neissex  23043  neiptoptop  23047  neiptopnei  23048  restbas  23074  tgrest  23075  restopnb  23091  cnpco  23183  isreg2  23293  iunconn  23344  1stcrest  23369  2ndcctbss  23371  2ndcomap  23374  2ndcsep  23375  dislly  23413  kgencn2  23473  ptbasfi  23497  txhaus  23563  txkgen  23568  txconn  23605  qtopcn  23630  regr1lem2  23656  kqnrmlem1  23659  kqnrmlem2  23660  trfbas2  23759  trfil2  23803  flimcf  23898  hauspwpwf1  23903  fclscf  23941  flimfnfcls  23944  ustexsym  24132  ustuqtop4  24160  utop3cls  24167  utopreg  24168  ucnima  24196  ucncn  24200  metequiv2  24426  prdsxmslem2  24445  metcnpi3  24462  metustto  24469  metustid  24470  metustexhalf  24472  ngptgp  24552  xrsblre  24728  icccmp  24742  reconnlem1  24743  reconn  24745  opnreen  24748  metdsf  24765  metdscn  24773  mpomulcn  24786  fsumcn  24789  elcncf2  24811  cncfmet  24830  pcoass  24952  lmcau  25241  rrxdstprj1  25337  pmltpc  25379  ivthlem2  25381  ivthlem3  25382  ovollb2  25418  volsup  25485  ioombl1  25491  ioorf  25502  dyadss  25523  dyaddisjlem  25524  dyadmax  25527  volcn  25535  cncombf  25587  mbflimsup  25595  itg2const2  25670  iblss2  25735  cpnord  25865  dvmptfsum  25907  fta1g  26103  plydivex  26233  fta1  26244  aannenlem1  26264  ulmdvlem3  26339  advlogexp  26592  cxpmul2z  26628  atantayl2  26876  jensen  26927  isppw2  27053  lgsqr  27290  lgsqrmodndvds  27292  lgsdchrval  27293  lgsquad3  27326  2sqb  27371  dchrisumlem3  27430  pntrsumbnd2  27506  noinfbnd1lem5  27667  noetasuplem4  27676  noetainflem4  27680  noetalem1  27681  conway  27741  eqscut3  27766  madebdayim  27834  madebdaylemlrcut  27845  negsprop  27978  mulscom  28079  absmuls  28183  bdayon  28210  remulscl  28405  tgjustf  28452  axsegcon  28906  axeuclidlem  28941  axcontlem9  28951  eengtrkg  28965  cusgrsize2inds  29433  pthdepisspth  29714  usgr2wlkneq  29735  crctcshwlkn0  29800  wpthswwlks2on  29940  clwwlkccatlem  29967  wwlksext2clwwlk  30035  umgr3v3e3cycl  30162  vdgn1frgrv2  30274  frgrwopreglem5  30299  frgrwopreg  30301  frgrhash2wsp  30310  numclwwlk1lem2fo  30336  vacn  30672  smcnlem  30675  0lno  30768  chocunii  31279  occl  31282  5oalem1  31632  3oalem2  31641  unoplin  31898  hmoplin  31920  lnconi  32011  kbass5  32098  mdslmd1lem1  32303  mdslmd1lem2  32304  mdsymlem2  32382  cdj1i  32411  opreu2reuALT  32454  unidifsnne  32514  disjabrex  32560  disjabrexf  32561  acunirnmpt  32639  fgreu  32652  suppovss  32660  xrge0infss  32741  xrofsup  32748  fsumiunle  32810  sgnmul  32816  sgnsub  32818  mgcf1o  32982  xrge0addgt0  32996  fzto1st1  33069  cyc3genpm  33119  cycpmgcl  33120  submarchi  33153  archiabllem1  33160  archiabllem2a  33161  isarchiofld  33166  rlocval  33224  imaslmod  33316  lindfpropd  33345  unitprodclb  33352  elrspunidl  33391  dfufd2lem  33512  lvecdim0  33617  constrmon  33755  constrextdg2  33760  locfinreflem  33851  zarcmplem  33892  rge0scvg  33960  lmxrge0  33963  lmdvg  33964  qqhval2  33993  esumrnmpt2  34079  esumfsup  34081  esumpcvgval  34089  esumcvg  34097  esumgect  34101  esumiun  34105  sigaclfu2  34132  sigainb  34147  insiga  34148  fiunelros  34185  measinblem  34231  measinb  34232  measdivcst  34235  measdivcstALTV  34236  omssubadd  34311  oddpwdc  34365  dstrvprob  34483  signsply0  34562  signstfvneq0  34583  bnj1408  35046  ptpconn  35275  sconnpi1  35281  resconn  35288  cvmliftmolem2  35324  cvmlift2lem12  35356  satfsschain  35406  satffunlem2lem1  35446  ifscgr  36084  cgrxfr  36095  outsideofeu  36171  linethru  36193  neibastop1  36399  dnicn  36532  irrdifflemf  37365  irrdiff  37366  fin2so  37653  matunitlindflem1  37662  matunitlindflem2  37663  poimirlem28  37694  poimirlem31  37697  mblfinlem2  37704  mblfinlem3  37705  itg2addnclem  37717  ftc1anclem7  37745  ftc1anclem8  37746  ftc1anc  37747  ssbnd  37834  totbndbnd  37835  prtlem10  38910  lssats  39057  lkrlss  39140  lshpset2N  39164  2dim  39515  islvol5  39624  paddasslem11  39875  pexmidlem8N  40022  ltrnid  40180  idltrn  40195  trlator0  40216  trlnidatb  40222  cdlemf2  40607  cdlemg2cex  40636  tendodi1  40829  tendodi2  40830  diblss  41215  dihopelvalcpre  41293  dih1dimatlem  41374  dihglblem6  41385  primrootscoprmpow  42138  posbezout  42139  aks6d1c4  42163  sticksstones22  42207  aks6d1c6isolem1  42213  aks6d1c6isolem2  42214  aks6d1c6lem5  42216  grpods  42233  unitscyglem3  42236  unitscyglem4  42237  remul01  42446  sn-subeu  42466  sn-0tie0  42490  prjspertr  42644  prjspersym  42646  0prjspnrel  42666  mzpsubst  42787  mzpcompact2lem  42790  eldioph2  42801  eldioph2b  42802  diophren  42852  pell14qrexpcl  42906  elpell1qr2  42911  monotoddzzfi  42981  acongtr  43017  acongrep  43019  jm2.19lem4  43031  jm2.26a  43039  jm2.26lem3  43040  jm2.26  43041  isnumbasgrplem2  43143  mendassa  43229  omord2lim  43339  cantnftermord  43359  tfsconcatfv1  43378  tfsconcatfv2  43379  naddcnffo  43403  naddcnfcom  43405  naddcnfid1  43406  naddgeoa  43433  clsk3nimkb  44079  prmunb2  44350  4an4132  44538  fiiuncl  45108  ssinc  45130  ssdec  45131  supxrgelem  45382  infxr  45411  cvgcaule  45535  mullimc  45662  mullimcf  45669  neglimc  45691  climleltrp  45720  climisp  45790  limsupresxr  45810  liminfresxr  45811  liminflimsupclim  45851  xlimliminflimsup  45906  icccncfext  45931  cncfiooicclem1  45937  fprodcncf  45944  dvnprodlem3  45992  iblcncfioo  46022  itgspltprt  46023  stoweidlem7  46051  stoweidlem28  46072  stoweidlem34  46078  stoweidlem48  46092  stoweidlem52  46096  wallispilem3  46111  fourierdlem12  46163  fourierdlem38  46189  fourierdlem39  46190  fourierdlem42  46193  fourierdlem46  46196  fourierdlem48  46198  fourierdlem49  46199  fourierdlem50  46200  fourierdlem51  46201  fourierdlem65  46215  fourierdlem73  46223  fourierdlem76  46226  fourierdlem87  46237  fourierdlem103  46253  fourierdlem104  46254  sge0f1o  46426  sge0le  46451  sge0reuz  46491  ismeannd  46511  isomenndlem  46574  hoicvr  46592  hoidmvle  46644  smflimlem2  46816  smflimmpt  46854  fsupdm  46886  finfdm  46890  imasetpreimafvbijlemf1  47441  nnsum4primeseven  47837  nnsum4primesevenALTV  47838  bgoldbtbndlem2  47843  bgoldbtbndlem3  47844  bgoldbtbnd  47846  isubgr3stgrlem6  48008  rrxlinec  48774  iccdisj  48935  upfval  49214  fullthinc  49488