Theorem simp-4r 783

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 733	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  8132  tfrlem1  8388  injresinj  13802  swrdccatin1  14741  reuccatpfxs1  14763  prdsval  17467  catcocl  17695  catass  17696  catpropd  17719  cidpropd  17720  monpropd  17748  subccocl  17856  funcco  17882  funcpropd  17913  fucpropd  17991  initoeu2lem1  18025  xpcpropd  18218  curf2ndf  18257  drsdirfi  18315  mhmmnd  19045  ghmqusnsg  19263  ghmquskerlem3  19267  gsmsymgreqlem2  19410  dfod2  19543  ghmcmn  19810  rhmqusnsg  21244  psgndif  21560  dmatscmcl  22439  smatvscl  22460  cpmatmcllem  22654  pm2mpmhmlem2  22755  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  neitr  23116  1stcrest  23389  dissnref  23464  dissnlocfin  23465  neitx  23543  tgqtop  23648  ptcmplem3  23990  trust  24166  utoptop  24171  restutopopn  24175  ustuqtop2  24179  ustuqtop4  24181  utop3cls  24188  met1stc  24458  prdsxmslem2  24466  metustexhalf  24493  cfilucfil  24496  metucn  24508  aannenlem1  26286  ulmuni  26351  lgamucov  26998  2sqmo  27398  pntpbnd  27549  pntlem3  27570  noetasuplem4  27698  noetainflem4  27702  tgbtwndiff  28431  tgifscgr  28433  iscgrglt  28439  tgbtwnconn1lem3  28499  tgbtwnconn1  28500  legov  28510  legtrd  28514  legtri3  28515  ltgseg  28521  legso  28524  tglinethru  28561  tglnpt2  28566  colline  28574  miriso  28595  midexlem  28617  perpneq  28639  isperp2  28640  footexALT  28643  footex  28646  midex  28662  opphllem3  28674  opphl  28679  hlpasch  28681  lnopp2hpgb  28688  lmieu  28709  trgcopyeu  28731  dfcgra2  28755  f1otrg  28796  axcontlem2  28890  2pthon3v  29871  2ndresdju  32573  fnpreimac  32595  fsumiunle  32754  ressprs  32890  dfmgc2  32922  mgcf1o  32929  chnind  32937  chnub  32938  chnso  32940  mndlrinvb  32966  mndlactf1o  32971  gsumfs2d  32995  gsumwun  33005  gsumwrd2dccatlem  33006  omndmul2  33026  tocyccntz  33101  cyc3genpm  33109  cycpmconjs  33113  cyc3conja  33114  isarchi3  33131  elrgspnlem4  33186  erler  33206  elrlocbasi  33207  rlocaddval  33209  rlocmulval  33210  rloccring  33211  rlocf1  33214  isdrng4  33235  fracfld  33248  isarchiofld  33285  imaslmod  33314  dvdsruasso  33346  nsgqusf1olem1  33374  nsgqusf1olem3  33376  lmhmqusker  33378  intlidl  33381  rhmquskerlem  33386  elrspunidl  33389  elrspunsn  33390  idlinsubrg  33392  rhmimaidl  33393  drngidl  33394  isprmidlc  33408  rhmpreimaprmidl  33412  qsidomlem2  33414  ssdifidllem  33417  ssdifidlprm  33419  mxidlprm  33431  mxidlirredi  33432  ssmxidllem  33434  ssmxidl  33435  opprqusplusg  33450  opprqusmulr  33452  qsdrngi  33456  qsdrng  33458  rsprprmprmidlb  33484  rprmdvdsprod  33495  1arithidom  33498  1arithufdlem2  33506  1arithufdlem3  33507  dfufd2lem  33510  r1plmhm  33565  r1pquslmic  33566  lbsdiflsp0  33612  dimkerim  33613  fedgmul  33617  fldextrspunlsplem  33660  constrconj  33725  constrfin  33726  constrelextdg2  33727  constrextdg2lem  33728  constrfiss  33731  ist0cld  33810  txomap  33811  qtophaus  33813  zarcls1  33846  zarclsint  33849  zarclssn  33850  pstmxmet  33874  sqsscirc1  33885  lmxrge0  33929  esumcst  34040  esumfsup  34047  esum2dlem  34069  esum2d  34070  esumiun  34071  ldsysgenld  34137  sigapildsys  34139  omssubadd  34278  signstfvneq0  34550  actfunsnf1o  34582  afsval  34649  nn0prpwlem  36286  lindsenlbs  37585  matunitlindflem1  37586  matunitlindflem2  37587  mblfinlem3  37629  itg2addnclem  37641  sstotbnd2  37744  prdstotbnd  37764  lcfl8  41467  fldhmf1  42049  mndmolinv  42054  primrootscoprmpow  42058  primrootspoweq0  42065  aks6d1c2p2  42078  aks6d1c2lem4  42086  aks6d1c2  42089  aks6d1c5  42098  aks6d1c6lem3  42131  unitscyglem3  42156  fiabv  42506  dffltz  42604  flt4lem7  42629  nna4b4nsq  42630  diophren  42783  rencldnfilem  42790  pellex  42805  pell1234qrdich  42831  pell1qrgap  42844  pellfundex  42856  omabs2  43303  iunconnlem2  44907  modelaxrep  44954  suplesup  45314  infleinflem2  45346  xrralrecnnle  45358  rexabslelem  45393  limcrecl  45606  limcleqr  45621  0ellimcdiv  45626  limclner  45628  limsupubuz  45690  limsupvaluz2  45715  supcnvlimsup  45717  climxrre  45727  xlimmnfvlem2  45810  xlimmnfv  45811  xlimpnfvlem2  45814  xlimpnfv  45815  icccncfext  45864  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  fourierdlem50  46133  fourierdlem51  46134  fourierdlem80  46163  fourierdlem87  46170  fourierdlem103  46186  fourierdlem104  46187  meaiuninc3v  46461  omef  46473  smflimlem2  46749  smflimlem4  46751  smfmullem3  46770  fsupdm  46819  finfdm  46823  imaf1co  49043  upfval  49059  fuco21  49195  prcofvalg  49235