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 731	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  7212  poseq  8101  oeeui  8531  oaabs2  8578  naddssim  8614  omxpenlem  9009  findcard3  9186  wemappo  9457  acndom2  9967  infpwfien  9975  sornom  10190  isf32lem2  10267  isf32lem4  10269  fin1a2lem11  10323  pwfseq  10578  gchina  10613  inttsk  10688  inar1  10689  prlem936  10961  mulcmpblnr  10985  00id  11312  mul02lem1  11313  addrid  11317  cnegex  11318  negeu  11374  add20  11653  ltmul12a  12002  lediv12a  12040  cru  12142  qextltlem  13145  xmullem  13207  xlemul1a  13231  ixxss12  13309  ioodisj  13426  elfz0fzfz0  13578  fsuppmapnn0fz  13949  seqf1o  13996  mulexpz  14055  leexp1a  14128  seqcoll  14417  swrdswrdlem  14657  pfxccatin12lem3  14685  abs3lem  15292  cau3lem  15308  climcau  15624  sumeq2ii  15646  climcndslem1  15805  climcndslem2  15806  geomulcvg  15832  mertenslem1  15840  mertenslem2  15841  mertens  15842  prodeq2ii  15867  prodmolem2  15891  bitsfzo  16395  sadadd2lem2  16410  dvdsmulgcd  16516  qredeu  16618  pc2dvds  16841  pcz  16843  ramcl  16991  firest  17386  mreexexlemd  17601  isacs2  17610  iscatd2  17638  ipodrsima  18498  mrelatlub  18519  mgmhmeql  18675  sgrppropd  18690  mndpropd  18718  mhmeql  18785  mhmid  19030  mhmmnd  19031  issubg4  19112  cycsubm  19168  cycsubmcom  19170  gasubg  19268  symgextf  19383  pmtr3ncom  19441  gexdvds  19550  oddvdssubg  19821  imasabl  19842  cyggeninv  19849  cyggenod  19850  submomnd  20098  issrg  20160  dvdsrmul1  20340  unitgrp  20354  cntzsubrng  20535  cntzsubr  20574  islmhm2  21025  lmhmeql  21042  lbspropd  21086  lssacsex  21134  rngqiprngimfo  21291  psgndiflemA  21591  isphl  21618  ocvocv  21661  lindfmm  21817  issubassa2  21882  mplbas2  22030  scmatmats  22486  smatvscl  22499  mdetdiag  22574  m2cpmfo  22731  pmatcollpw3fi1lem1  22761  pm2mpf1  22774  pm2mpghm  22791  fvmptnn04if  22824  chfacfscmulfsupp  22834  chfacfpmmulfsupp  22838  neissex  23102  neiptoptop  23106  neiptopnei  23107  restbas  23133  tgrest  23134  restopnb  23150  cnpco  23242  isreg2  23352  iunconn  23403  1stcrest  23428  2ndcctbss  23430  2ndcomap  23433  2ndcsep  23434  dislly  23472  kgencn2  23532  ptbasfi  23556  txhaus  23622  txkgen  23627  txconn  23664  qtopcn  23689  regr1lem2  23715  kqnrmlem1  23718  kqnrmlem2  23719  trfbas2  23818  trfil2  23862  flimcf  23957  hauspwpwf1  23962  fclscf  24000  flimfnfcls  24003  ustexsym  24191  ustuqtop4  24219  utop3cls  24226  utopreg  24227  ucnima  24255  ucncn  24259  metequiv2  24485  prdsxmslem2  24504  metcnpi3  24521  metustto  24528  metustid  24529  metustexhalf  24531  ngptgp  24611  xrsblre  24787  icccmp  24801  reconnlem1  24802  reconn  24804  opnreen  24807  metdsf  24824  metdscn  24832  mpomulcn  24844  fsumcn  24847  elcncf2  24867  cncfmet  24886  pcoass  25001  lmcau  25290  rrxdstprj1  25386  pmltpc  25427  ivthlem2  25429  ivthlem3  25430  ovollb2  25466  volsup  25533  ioombl1  25539  ioorf  25550  dyadss  25571  dyaddisjlem  25572  dyadmax  25575  volcn  25583  cncombf  25635  mbflimsup  25643  itg2const2  25718  iblss2  25783  cpnord  25912  dvmptfsum  25952  fta1g  26145  plydivex  26274  fta1  26285  aannenlem1  26305  ulmdvlem3  26380  advlogexp  26632  cxpmul2z  26668  atantayl2  26915  jensen  26966  isppw2  27092  lgsqr  27328  lgsqrmodndvds  27330  lgsdchrval  27331  lgsquad3  27364  2sqb  27409  dchrisumlem3  27468  pntrsumbnd2  27544  noinfbnd1lem5  27705  noetasuplem4  27714  noetainflem4  27718  noetalem1  27719  conway  27785  eqcuts3  27810  madebdayim  27894  madebdaylemlrcut  27905  negsprop  28041  mulscom  28145  absmuls  28250  bdayons  28282  addonbday  28285  bdayfinbndlem1  28473  remulscl  28508  tgjustf  28555  axsegcon  29010  axeuclidlem  29045  axcontlem9  29055  eengtrkg  29069  cusgrsize2inds  29537  pthdepisspth  29818  usgr2wlkneq  29839  crctcshwlkn0  29904  wpthswwlks2on  30047  clwwlkccatlem  30074  wwlksext2clwwlk  30142  umgr3v3e3cycl  30269  vdgn1frgrv2  30381  frgrwopreglem5  30406  frgrwopreg  30408  frgrhash2wsp  30417  numclwwlk1lem2fo  30443  vacn  30780  smcnlem  30783  0lno  30876  chocunii  31387  occl  31390  5oalem1  31740  3oalem2  31749  unoplin  32006  hmoplin  32028  lnconi  32119  kbass5  32206  mdslmd1lem1  32411  mdslmd1lem2  32412  mdsymlem2  32490  cdj1i  32519  opreu2reuALT  32561  unidifsnne  32621  disjabrex  32667  disjabrexf  32668  acunirnmpt  32747  fgreu  32759  suppovss  32769  xrge0infss  32848  xrofsup  32855  fsumiunle  32917  sgnmul  32923  sgnsub  32925  mgcf1o  33078  xrge0addgt0  33092  fzto1st1  33178  cyc3genpm  33228  cycpmgcl  33229  submarchi  33262  archiabllem1  33269  archiabllem2a  33270  isarchiofld  33275  rlocval  33335  imaslmod  33428  lindfpropd  33457  unitprodclb  33464  elrspunidl  33503  dfufd2lem  33624  mplmulmvr  33698  lvecdim0  33766  constrmon  33904  constrextdg2  33909  locfinreflem  34000  zarcmplem  34041  rge0scvg  34109  lmxrge0  34112  lmdvg  34113  qqhval2  34142  esumrnmpt2  34228  esumfsup  34230  esumpcvgval  34238  esumcvg  34246  esumgect  34250  esumiun  34254  sigaclfu2  34281  sigainb  34296  insiga  34297  fiunelros  34334  measinblem  34380  measinb  34381  measdivcst  34384  measdivcstALTV  34385  omssubadd  34460  oddpwdc  34514  dstrvprob  34632  signsply0  34711  signstfvneq0  34732  bnj1408  35194  ptpconn  35431  sconnpi1  35437  resconn  35444  cvmliftmolem2  35480  cvmlift2lem12  35512  satfsschain  35562  satffunlem2lem1  35602  ifscgr  36242  cgrxfr  36253  outsideofeu  36329  linethru  36351  neibastop1  36557  dnicn  36768  irrdifflemf  37655  irrdiff  37656  fin2so  37942  matunitlindflem1  37951  matunitlindflem2  37952  poimirlem28  37983  poimirlem31  37986  mblfinlem2  37993  mblfinlem3  37994  itg2addnclem  38006  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  ssbnd  38123  totbndbnd  38124  prtlem10  39325  lssats  39472  lkrlss  39555  lshpset2N  39579  2dim  39930  islvol5  40039  paddasslem11  40290  pexmidlem8N  40437  ltrnid  40595  idltrn  40610  trlator0  40631  trlnidatb  40637  cdlemf2  41022  cdlemg2cex  41051  tendodi1  41244  tendodi2  41245  diblss  41630  dihopelvalcpre  41708  dih1dimatlem  41789  dihglblem6  41800  primrootscoprmpow  42552  posbezout  42553  aks6d1c4  42577  sticksstones22  42621  aks6d1c6isolem1  42627  aks6d1c6isolem2  42628  aks6d1c6lem5  42630  grpods  42647  unitscyglem3  42650  unitscyglem4  42651  remul01  42853  sn-subeu  42873  sn-0tie0  42910  prjspertr  43052  prjspersym  43054  0prjspnrel  43074  mzpsubst  43194  mzpcompact2lem  43197  eldioph2  43208  eldioph2b  43209  diophren  43259  pell14qrexpcl  43313  elpell1qr2  43318  monotoddzzfi  43388  acongtr  43424  acongrep  43426  jm2.19lem4  43438  jm2.26a  43446  jm2.26lem3  43447  jm2.26  43448  isnumbasgrplem2  43550  mendassa  43636  omord2lim  43746  cantnftermord  43766  tfsconcatfv1  43785  tfsconcatfv2  43786  naddcnffo  43810  naddcnfcom  43812  naddcnfid1  43813  naddgeoa  43840  clsk3nimkb  44485  prmunb2  44756  4an4132  44944  fiiuncl  45514  ssinc  45535  ssdec  45536  supxrgelem  45785  infxr  45814  cvgcaule  45937  mullimc  46064  mullimcf  46071  neglimc  46093  climleltrp  46122  climisp  46192  limsupresxr  46212  liminfresxr  46213  liminflimsupclim  46253  xlimliminflimsup  46308  icccncfext  46333  cncfiooicclem1  46339  fprodcncf  46346  dvnprodlem3  46394  iblcncfioo  46424  itgspltprt  46425  stoweidlem7  46453  stoweidlem28  46474  stoweidlem34  46480  stoweidlem48  46494  stoweidlem52  46498  wallispilem3  46513  fourierdlem12  46565  fourierdlem38  46591  fourierdlem39  46592  fourierdlem42  46595  fourierdlem46  46598  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem51  46603  fourierdlem65  46617  fourierdlem73  46625  fourierdlem76  46628  fourierdlem87  46639  fourierdlem103  46655  fourierdlem104  46656  sge0f1o  46828  sge0le  46853  sge0reuz  46893  ismeannd  46913  isomenndlem  46976  hoicvr  46994  hoidmvle  47046  smflimlem2  47218  smflimmpt  47256  fsupdm  47288  finfdm  47292  nndivides2  47844  imasetpreimafvbijlemf1  47876  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  bgoldbtbnd  48297  isubgr3stgrlem6  48459  rrxlinec  49224  iccdisj  49385  upfval  49663  fullthinc  49937