Theorem simp-4r 784

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)

Assertion

Ref	Expression
simp-4r	⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem simp-4r

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad4antlr 734	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:  fimaproj  8087  tfrlem1  8317  injresinj  13719  swrdccatin1  14660  reuccatpfxs1  14682  prdsval  17387  catcocl  17620  catass  17621  catpropd  17644  cidpropd  17645  monpropd  17673  subccocl  17781  funcco  17807  funcpropd  17838  fucpropd  17916  initoeu2lem1  17950  xpcpropd  18143  curf2ndf  18182  drsdirfi  18240  chnind  18556  chnub  18557  chnso  18559  mhmmnd  19006  ghmqusnsg  19223  ghmquskerlem3  19227  gsmsymgreqlem2  19372  dfod2  19505  ghmcmn  19772  omndmul2  20074  rhmqusnsg  21252  psgndif  21569  dmatscmcl  22459  smatvscl  22480  cpmatmcllem  22674  pm2mpmhmlem2  22775  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  neitr  23136  1stcrest  23409  dissnref  23484  dissnlocfin  23485  neitx  23563  tgqtop  23668  ptcmplem3  24010  trust  24185  utoptop  24190  restutopopn  24194  ustuqtop2  24198  ustuqtop4  24200  utop3cls  24207  met1stc  24477  prdsxmslem2  24485  metustexhalf  24512  cfilucfil  24515  metucn  24527  aannenlem1  26304  ulmuni  26369  lgamucov  27016  2sqmo  27416  pntpbnd  27567  pntlem3  27588  noetasuplem4  27716  noetainflem4  27720  bdayfinbndlem1  28475  tgbtwndiff  28590  tgifscgr  28592  iscgrglt  28598  tgbtwnconn1lem3  28658  tgbtwnconn1  28659  legov  28669  legtrd  28673  legtri3  28674  ltgseg  28680  legso  28683  tglinethru  28720  tglnpt2  28725  colline  28733  miriso  28754  midexlem  28776  perpneq  28798  isperp2  28799  footexALT  28802  footex  28805  midex  28821  opphllem3  28833  opphl  28838  hlpasch  28840  lnopp2hpgb  28847  lmieu  28868  trgcopyeu  28890  dfcgra2  28914  f1otrg  28955  axcontlem2  29050  2pthon3v  30028  2ndresdju  32738  fnpreimac  32759  fsumiunle  32920  ressprs  33058  dfmgc2  33088  mgcf1o  33095  mndlrinvb  33117  mndlactf1o  33122  gsumfs2d  33154  gsumwun  33169  gsumwrd2dccatlem  33170  tocyccntz  33237  cyc3genpm  33245  cycpmconjs  33249  cyc3conja  33250  isarchi3  33280  isarchiofld  33292  elrgspnlem4  33338  erler  33358  elrlocbasi  33359  rlocaddval  33361  rlocmulval  33362  rloccring  33363  rlocf1  33366  isdrng4  33388  fracfld  33401  imaslmod  33445  dvdsruasso  33477  nsgqusf1olem1  33505  nsgqusf1olem3  33507  lmhmqusker  33509  intlidl  33512  rhmquskerlem  33517  elrspunidl  33520  elrspunsn  33521  idlinsubrg  33523  rhmimaidl  33524  drngidl  33525  isprmidlc  33539  rhmpreimaprmidl  33543  qsidomlem2  33545  ssdifidllem  33548  ssdifidlprm  33550  mxidlprm  33562  mxidlirredi  33563  ssmxidllem  33565  ssmxidl  33566  opprqusplusg  33581  opprqusmulr  33583  qsdrngi  33587  qsdrng  33589  rsprprmprmidlb  33615  rprmdvdsprod  33626  1arithidom  33629  1arithufdlem2  33637  1arithufdlem3  33638  dfufd2lem  33641  r1plmhm  33702  r1pquslmic  33703  lbsdiflsp0  33803  dimkerim  33804  fedgmul  33808  fldextrspunlsplem  33850  extdgfialg  33871  constrconj  33922  constrfin  33923  constrelextdg2  33924  constrextdg2lem  33925  constrfiss  33928  ist0cld  34010  txomap  34011  qtophaus  34013  zarcls1  34046  zarclsint  34049  zarclssn  34050  pstmxmet  34074  sqsscirc1  34085  lmxrge0  34129  esumcst  34240  esumfsup  34247  esum2dlem  34269  esum2d  34270  esumiun  34271  ldsysgenld  34337  sigapildsys  34339  omssubadd  34477  signstfvneq0  34749  actfunsnf1o  34781  afsval  34848  nn0prpwlem  36535  lindsenlbs  37860  matunitlindflem1  37861  matunitlindflem2  37862  mblfinlem3  37904  itg2addnclem  37916  sstotbnd2  38019  prdstotbnd  38039  lcfl8  41872  fldhmf1  42454  mndmolinv  42459  primrootscoprmpow  42463  primrootspoweq0  42470  aks6d1c2p2  42483  aks6d1c2lem4  42491  aks6d1c2  42494  aks6d1c5  42503  aks6d1c6lem3  42536  unitscyglem3  42561  fiabv  42900  dffltz  42986  flt4lem7  43011  nna4b4nsq  43012  diophren  43164  rencldnfilem  43171  pellex  43186  pell1234qrdich  43212  pell1qrgap  43225  pellfundex  43237  omabs2  43683  iunconnlem2  45284  modelaxrep  45331  suplesup  45692  infleinflem2  45723  xrralrecnnle  45735  rexabslelem  45770  limcrecl  45983  limcleqr  45996  0ellimcdiv  46001  limclner  46003  limsupubuz  46065  limsupvaluz2  46090  supcnvlimsup  46092  climxrre  46102  xlimmnfvlem2  46185  xlimmnfv  46186  xlimpnfvlem2  46189  xlimpnfv  46190  icccncfext  46239  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  fourierdlem50  46508  fourierdlem51  46509  fourierdlem80  46538  fourierdlem87  46545  fourierdlem103  46561  fourierdlem104  46562  meaiuninc3v  46836  omef  46848  smflimlem2  47124  smflimlem4  47126  smfmullem3  47145  fsupdm  47194  finfdm  47198  chnerlem1  47234  imaf1co  49508  upfval  49529  fuco21  49689  prcofvalg  49729