Theorem simplll 775

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  7283  poseq  8181  oeeui  8638  oaabs2  8685  naddssim  8721  omxpenlem  9111  findcard3  9315  wemappo  9586  acndom2  10091  infpwfien  10099  sornom  10314  isf32lem2  10391  isf32lem4  10393  fin1a2lem11  10447  pwfseq  10701  gchina  10736  inttsk  10811  inar1  10812  prlem936  11084  mulcmpblnr  11108  00id  11433  mul02lem1  11434  addrid  11438  cnegex  11439  negeu  11495  add20  11772  ltmul12a  12120  lediv12a  12158  cru  12255  qextltlem  13240  xmullem  13302  xlemul1a  13326  ixxss12  13403  ioodisj  13518  elfz0fzfz0  13669  fsuppmapnn0fz  14033  seqf1o  14080  mulexpz  14139  leexp1a  14211  seqcoll  14499  swrdswrdlem  14738  pfxccatin12lem3  14766  abs3lem  15373  cau3lem  15389  climcau  15703  sumeq2ii  15725  climcndslem1  15881  climcndslem2  15882  geomulcvg  15908  mertenslem1  15916  mertenslem2  15917  mertens  15918  prodeq2ii  15943  prodmolem2  15967  bitsfzo  16468  sadadd2lem2  16483  dvdsmulgcd  16589  qredeu  16691  pc2dvds  16912  pcz  16914  ramcl  17062  firest  17478  mreexexlemd  17688  isacs2  17697  iscatd2  17725  ipodrsima  18598  mrelatlub  18619  mgmhmeql  18741  sgrppropd  18756  mndpropd  18784  mhmeql  18851  mhmid  19093  mhmmnd  19094  issubg4  19175  cycsubm  19232  cycsubmcom  19234  gasubg  19332  symgextf  19449  pmtr3ncom  19507  gexdvds  19616  oddvdssubg  19887  imasabl  19908  cyggeninv  19915  cyggenod  19916  issrg  20205  dvdsrmul1  20385  unitgrp  20399  cntzsubrng  20583  cntzsubr  20622  islmhm2  21054  lmhmeql  21071  lbspropd  21115  lssacsex  21163  rngqiprngimfo  21328  psgndiflemA  21636  isphl  21663  ocvocv  21706  lindfmm  21864  issubassa2  21929  mplbas2  22077  scmatmats  22532  smatvscl  22545  mdetdiag  22620  m2cpmfo  22777  pmatcollpw3fi1lem1  22807  pm2mpf1  22820  pm2mpghm  22837  fvmptnn04if  22870  chfacfscmulfsupp  22880  chfacfpmmulfsupp  22884  neissex  23150  neiptoptop  23154  neiptopnei  23155  restbas  23181  tgrest  23182  restopnb  23198  cnpco  23290  isreg2  23400  iunconn  23451  1stcrest  23476  2ndcctbss  23478  2ndcomap  23481  2ndcsep  23482  dislly  23520  kgencn2  23580  ptbasfi  23604  txhaus  23670  txkgen  23675  txconn  23712  qtopcn  23737  regr1lem2  23763  kqnrmlem1  23766  kqnrmlem2  23767  trfbas2  23866  trfil2  23910  flimcf  24005  hauspwpwf1  24010  fclscf  24048  flimfnfcls  24051  ustexsym  24239  ustuqtop4  24268  utop3cls  24275  utopreg  24276  ucnima  24305  ucncn  24309  metequiv2  24538  prdsxmslem2  24557  metcnpi3  24574  metustto  24581  metustid  24582  metustexhalf  24584  ngptgp  24664  xrsblre  24846  icccmp  24860  reconnlem1  24861  reconn  24863  opnreen  24866  metdsf  24883  metdscn  24891  mpomulcn  24904  fsumcn  24907  elcncf2  24929  cncfmet  24948  pcoass  25070  lmcau  25360  rrxdstprj1  25456  pmltpc  25498  ivthlem2  25500  ivthlem3  25501  ovollb2  25537  volsup  25604  ioombl1  25610  ioorf  25621  dyadss  25642  dyaddisjlem  25643  dyadmax  25646  volcn  25654  cncombf  25706  mbflimsup  25714  itg2const2  25790  iblss2  25855  cpnord  25985  dvmptfsum  26027  fta1g  26223  plydivex  26353  fta1  26364  aannenlem1  26384  ulmdvlem3  26459  advlogexp  26711  cxpmul2z  26747  atantayl2  26995  jensen  27046  isppw2  27172  lgsqr  27409  lgsqrmodndvds  27411  lgsdchrval  27412  lgsquad3  27445  2sqb  27490  dchrisumlem3  27549  pntrsumbnd2  27625  noinfbnd1lem5  27786  noetasuplem4  27795  noetainflem4  27799  noetalem1  27800  conway  27858  madebdayim  27940  madebdaylemlrcut  27951  negsprop  28081  mulscom  28179  absmuls  28282  remulscl  28448  tgjustf  28495  axsegcon  28956  axeuclidlem  28991  axcontlem9  29001  eengtrkg  29015  cusgrsize2inds  29485  pthdepisspth  29767  usgr2wlkneq  29788  crctcshwlkn0  29850  wpthswwlks2on  29990  clwwlkccatlem  30017  wwlksext2clwwlk  30085  umgr3v3e3cycl  30212  vdgn1frgrv2  30324  frgrwopreglem5  30349  frgrwopreg  30351  frgrhash2wsp  30360  numclwwlk1lem2fo  30386  vacn  30722  smcnlem  30725  0lno  30818  chocunii  31329  occl  31332  5oalem1  31682  3oalem2  31691  unoplin  31948  hmoplin  31970  lnconi  32061  kbass5  32148  mdslmd1lem1  32353  mdslmd1lem2  32354  mdsymlem2  32432  cdj1i  32461  opreu2reuALT  32504  unidifsnne  32561  disjabrex  32601  disjabrexf  32602  acunirnmpt  32675  fgreu  32688  suppovss  32695  xrge0infss  32770  xrofsup  32777  fsumiunle  32835  mgcf1o  32977  xrge0addgt0  33004  submomnd  33069  fzto1st1  33104  cyc3genpm  33154  cycpmgcl  33155  submarchi  33175  archiabllem1  33182  archiabllem2a  33183  rlocval  33245  isarchiofld  33326  imaslmod  33360  lindfpropd  33389  unitprodclb  33396  elrspunidl  33435  dfufd2lem  33556  lvecdim0  33633  constrmon  33748  locfinreflem  33800  zarcmplem  33841  rge0scvg  33909  lmxrge0  33912  lmdvg  33913  qqhval2  33944  esumrnmpt2  34048  esumfsup  34050  esumpcvgval  34058  esumcvg  34066  esumgect  34070  esumiun  34074  sigaclfu2  34101  sigainb  34116  insiga  34117  fiunelros  34154  measinblem  34200  measinb  34201  measdivcst  34204  measdivcstALTV  34205  omssubadd  34281  oddpwdc  34335  dstrvprob  34452  sgnmul  34523  sgnsub  34525  signsply0  34544  signstfvneq0  34565  bnj1408  35028  ptpconn  35217  sconnpi1  35223  resconn  35230  cvmliftmolem2  35266  cvmlift2lem12  35298  satfsschain  35348  satffunlem2lem1  35388  ifscgr  36025  cgrxfr  36036  outsideofeu  36112  linethru  36134  neibastop1  36341  dnicn  36474  irrdifflemf  37307  irrdiff  37308  fin2so  37593  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem28  37634  poimirlem31  37637  mblfinlem2  37644  mblfinlem3  37645  itg2addnclem  37657  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  ssbnd  37774  totbndbnd  37775  prtlem10  38846  lssats  38993  lkrlss  39076  lshpset2N  39100  2dim  39452  islvol5  39561  paddasslem11  39812  pexmidlem8N  39959  ltrnid  40117  idltrn  40132  trlator0  40153  trlnidatb  40159  cdlemf2  40544  cdlemg2cex  40573  tendodi1  40766  tendodi2  40767  diblss  41152  dihopelvalcpre  41230  dih1dimatlem  41311  dihglblem6  41322  primrootscoprmpow  42080  posbezout  42081  aks6d1c4  42105  sticksstones22  42149  aks6d1c6isolem1  42155  aks6d1c6isolem2  42156  aks6d1c6lem5  42158  grpods  42175  unitscyglem3  42178  unitscyglem4  42179  remul01  42413  sn-subeu  42432  sn-0tie0  42445  sn-itrere  42474  sn-retire  42475  prjspertr  42591  prjspersym  42593  0prjspnrel  42613  mzpsubst  42735  mzpcompact2lem  42738  eldioph2  42749  eldioph2b  42750  diophren  42800  pell14qrexpcl  42854  elpell1qr2  42859  monotoddzzfi  42930  acongtr  42966  acongrep  42968  jm2.19lem4  42980  jm2.26a  42988  jm2.26lem3  42989  jm2.26  42990  isnumbasgrplem2  43092  mendassa  43178  omord2lim  43289  cantnftermord  43309  tfsconcatfv1  43328  tfsconcatfv2  43329  naddcnffo  43353  naddcnfcom  43355  naddcnfid1  43356  naddgeoa  43383  clsk3nimkb  44029  prmunb2  44306  4an4132  44496  fiiuncl  45004  ssinc  45026  ssdec  45027  supxrgelem  45286  infxr  45316  cvgcaule  45441  mullimc  45571  mullimcf  45578  neglimc  45602  climleltrp  45631  climisp  45701  limsupresxr  45721  liminfresxr  45722  liminflimsupclim  45762  xlimliminflimsup  45817  icccncfext  45842  cncfiooicclem1  45848  fprodcncf  45855  dvnprodlem3  45903  iblcncfioo  45933  itgspltprt  45934  stoweidlem7  45962  stoweidlem28  45983  stoweidlem34  45989  stoweidlem48  46003  stoweidlem52  46007  wallispilem3  46022  fourierdlem12  46074  fourierdlem38  46100  fourierdlem39  46101  fourierdlem42  46104  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem51  46112  fourierdlem65  46126  fourierdlem73  46134  fourierdlem76  46137  fourierdlem87  46148  fourierdlem103  46164  fourierdlem104  46165  sge0f1o  46337  sge0le  46362  sge0reuz  46402  ismeannd  46422  isomenndlem  46485  hoicvr  46503  hoidmvle  46555  smflimlem2  46727  smflimmpt  46765  fsupdm  46797  finfdm  46801  imasetpreimafvbijlemf1  47328  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbnd  47733  isubgr3stgrlem6  47873  rrxlinec  48585  iccdisj  48694  fullthinc  48845