Theorem simp-5r 786

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

Assertion

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

Proof of Theorem simp-5r

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad5antlr 735	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:  catcocl  17730  catass  17731  monpropd  17785  subccocl  17896  funcco  17922  funcpropd  17954  mhmmnd  19095  ghmqusnsg  19313  ghmquskerlem3  19317  rhmqusnsg  21313  pm2mpmhmlem2  22841  neitr  23204  restutopopn  24263  ustuqtop4  24269  utopreg  24277  cfilucfil  24588  psmetutop  24596  dyadmax  25647  2sqmo  27496  tgifscgr  28531  tgcgrxfr  28541  tgbtwnconn1lem3  28597  tgbtwnconn1  28598  legov  28608  legtrd  28612  legso  28622  miriso  28693  perpneq  28737  footexALT  28741  footex  28744  colperpex  28756  opphllem  28758  midex  28760  opphl  28777  lnopp2hpgb  28786  trgcopyeu  28829  dfcgra2  28853  inaghl  28868  f1otrg  28894  2ndresdju  32666  nn0xmulclb  32782  chnub  32986  omndmul2  33072  psgnfzto1stlem  33103  cyc3genpm  33155  elrgspnlem4  33235  rloccring  33257  rlocf1  33260  dvdsruasso  33393  nsgqusf1olem3  33423  rhmquskerlem  33433  elrspunidl  33436  rhmimaidl  33440  rhmpreimaprmidl  33459  ssdifidllem  33464  ssdifidlprm  33466  mxidlprm  33478  mxidlirredi  33479  ssmxidl  33482  qsdrngi  33503  qsdrng  33505  1arithidom  33545  1arithufdlem3  33554  r1plmhm  33610  r1pquslmic  33611  lbsdiflsp0  33654  fldext2chn  33734  constrconj  33750  constrfin  33751  constrelextdg2  33752  qtophaus  33797  locfinreflem  33801  cmpcref  33811  pstmxmet  33858  lmxrge0  33913  esumcst  34044  omssubadd  34282  signstfvneq0  34566  afsval  34665  matunitlindflem1  37603  heicant  37642  sstotbnd2  37761  primrootscoprmpow  42081  primrootspoweq0  42088  aks6d1c2p2  42101  aks6d1c2lem4  42109  aks6d1c2  42112  unitscyglem3  42179  dffltz  42621  flt4lem7  42646  eldioph2b  42751  diophren  42801  pell1234qrdich  42849  omabs2  43322  iunconnlem2  44933  limcrecl  45585  limclner  45607  icccncfext  45843  ioodvbdlimc1lem2  45888  ioodvbdlimc2lem  45890  stoweidlem60  46016  fourierdlem51  46113  fourierdlem77  46139  fourierdlem103  46165  fourierdlem104  46166  smfaddlem1  46719  smfmullem3  46749  grtriprop  47846