Theorem simp-5r 785

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  17699  catass  17700  monpropd  17752  subccocl  17861  funcco  17887  funcpropd  17918  mhmmnd  19051  ghmqusnsg  19269  ghmquskerlem3  19273  rhmqusnsg  21257  pm2mpmhmlem2  22773  neitr  23134  restutopopn  24193  ustuqtop4  24199  utopreg  24207  cfilucfil  24516  psmetutop  24524  dyadmax  25569  2sqmo  27417  tgifscgr  28452  tgcgrxfr  28462  tgbtwnconn1lem3  28518  tgbtwnconn1  28519  legov  28529  legtrd  28533  legso  28543  miriso  28614  perpneq  28658  footexALT  28662  footex  28665  colperpex  28677  opphllem  28679  midex  28681  opphl  28698  lnopp2hpgb  28707  trgcopyeu  28750  dfcgra2  28774  inaghl  28789  f1otrg  28815  2ndresdju  32594  nn0xmulclb  32712  chnub  32941  omndmul2  33028  psgnfzto1stlem  33059  cyc3genpm  33111  elrgspnlem4  33188  rloccring  33213  rlocf1  33216  dvdsruasso  33348  nsgqusf1olem3  33378  rhmquskerlem  33388  elrspunidl  33391  rhmimaidl  33395  rhmpreimaprmidl  33414  ssdifidllem  33419  ssdifidlprm  33421  mxidlprm  33433  mxidlirredi  33434  ssmxidl  33437  qsdrngi  33458  qsdrng  33460  1arithidom  33500  1arithufdlem3  33509  r1plmhm  33565  r1pquslmic  33566  lbsdiflsp0  33612  fldext2chn  33708  constrconj  33725  constrfin  33726  constrelextdg2  33727  constrfiss  33731  qtophaus  33794  locfinreflem  33798  cmpcref  33808  pstmxmet  33855  lmxrge0  33910  esumcst  34023  omssubadd  34261  signstfvneq0  34546  afsval  34645  matunitlindflem1  37582  heicant  37621  sstotbnd2  37740  primrootscoprmpow  42059  primrootspoweq0  42066  aks6d1c2p2  42079  aks6d1c2lem4  42087  aks6d1c2  42090  unitscyglem3  42157  dffltz  42607  flt4lem7  42632  eldioph2b  42737  diophren  42787  pell1234qrdich  42835  omabs2  43307  iunconnlem2  44912  limcrecl  45601  limclner  45623  icccncfext  45859  ioodvbdlimc1lem2  45904  ioodvbdlimc2lem  45906  stoweidlem60  46032  fourierdlem51  46129  fourierdlem77  46155  fourierdlem103  46181  fourierdlem104  46182  smfaddlem1  46735  smfmullem3  46765  grtriprop  47866  upfval  48904  fuco21  49007