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  17653  catass  17654  monpropd  17706  subccocl  17814  funcco  17840  funcpropd  17871  mhmmnd  19003  ghmqusnsg  19221  ghmquskerlem3  19225  rhmqusnsg  21202  pm2mpmhmlem2  22713  neitr  23074  restutopopn  24133  ustuqtop4  24139  utopreg  24147  cfilucfil  24454  psmetutop  24462  dyadmax  25506  2sqmo  27355  tgifscgr  28442  tgcgrxfr  28452  tgbtwnconn1lem3  28508  tgbtwnconn1  28509  legov  28519  legtrd  28523  legso  28533  miriso  28604  perpneq  28648  footexALT  28652  footex  28655  colperpex  28667  opphllem  28669  midex  28671  opphl  28688  lnopp2hpgb  28697  trgcopyeu  28740  dfcgra2  28764  inaghl  28779  f1otrg  28805  2ndresdju  32580  nn0xmulclb  32701  chnub  32945  omndmul2  33033  psgnfzto1stlem  33064  cyc3genpm  33116  elrgspnlem4  33203  rloccring  33228  rlocf1  33231  dvdsruasso  33363  nsgqusf1olem3  33393  rhmquskerlem  33403  elrspunidl  33406  rhmimaidl  33410  rhmpreimaprmidl  33429  ssdifidllem  33434  ssdifidlprm  33436  mxidlprm  33448  mxidlirredi  33449  ssmxidl  33452  qsdrngi  33473  qsdrng  33475  1arithidom  33515  1arithufdlem3  33524  r1plmhm  33582  r1pquslmic  33583  lbsdiflsp0  33629  fldext2chn  33725  constrconj  33742  constrfin  33743  constrelextdg2  33744  constrfiss  33748  cos9thpiminplylem2  33780  qtophaus  33833  locfinreflem  33837  cmpcref  33847  pstmxmet  33894  lmxrge0  33949  esumcst  34060  omssubadd  34298  signstfvneq0  34570  afsval  34669  matunitlindflem1  37617  heicant  37656  sstotbnd2  37775  primrootscoprmpow  42094  primrootspoweq0  42101  aks6d1c2p2  42114  aks6d1c2lem4  42122  aks6d1c2  42125  unitscyglem3  42192  dffltz  42629  flt4lem7  42654  eldioph2b  42758  diophren  42808  pell1234qrdich  42856  omabs2  43328  iunconnlem2  44931  limcrecl  45634  limclner  45656  icccncfext  45892  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  stoweidlem60  46065  fourierdlem51  46162  fourierdlem77  46188  fourierdlem103  46214  fourierdlem104  46215  smfaddlem1  46768  smfmullem3  46798  grtriprop  47944  upfval  49169  fuco21  49329