Theorem simp-5r 798

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 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	ad5antlr 748	1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  catcocl  17766  catass  17767  monpropd  17819  subccocl  17927  funcco  17953  funcpropd  17984  chnub  18703  mhmmnd  19161  ghmqusnsg  19383  ghmquskerlem3  19387  omndmul2  20234  rhmqusnsg  21462  rhmpreimaprmidl  21516  ssdifidllem  21521  ssdifidlprm  21523  pm2mpmhmlem2  23013  neitr  23374  restutopopn  24432  ustuqtop4  24438  utopreg  24446  cfilucfil  24753  psmetutop  24761  dyadmax  25794  2sqmo  27638  tgifscgr  28814  tgcgrxfr  28824  tgbtwnconn1lem3  28880  tgbtwnconn1  28881  legov  28891  legtrd  28895  legso  28905  miriso  28984  perpneq  29031  footexALT  29035  footex  29038  colperpex  29051  opphllem  29053  midex  29055  opphl  29072  lnopp2hpgb  29082  trgcopyeu  29154  dfcgra2  29178  ragcgra  29183  cgrarag  29184  ragsupplcgra  29185  inaghl  29199  perpprlng  29237  prlngmolem1  29239  prlngmolem2  29240  prlngmo2  29243  f1otrg  29257  2ndresdju  33031  nn0xmulclb  33153  psgnfzto1stlem  33451  cyc3genpm  33503  elrgspnlem4  33596  rloccring  33622  rlocf1  33625  ricdomn1  33640  dvdsruasso  33729  nsgqusf1olem3  33755  rhmquskerlem  33764  elrspunidl  33767  rhmimaidl  33771  mxidlprm  33784  mxidlirredi  33785  ssmxidl  33788  qsdrngi  33808  qsdrng  33810  1arithidom  33858  1arithufdlem3  33867  r1plmhm  33930  r1pquslmic  33931  mplidomlem  33948  vieta  34001  lbsdiflsp0  34047  fldext2chn  34149  constrconj  34166  constrfin  34167  constrelextdg2  34168  constrfiss  34172  cos9thpiminplylem2  34204  qtophaus  34257  locfinreflem  34261  cmpcref  34271  pstmxmet  34318  lmxrge0  34373  esumcst  34484  omssubadd  34722  signstfvneq0  34991  afsval  35093  matunitlindflem1  38308  heicant  38347  sstotbnd2  38466  primrootscoprmpow  42907  primrootspoweq0  42914  aks6d1c2p2  42927  aks6d1c2lem4  42935  aks6d1c2  42938  unitscyglem3  43005  dffltz  43407  flt4lem7  43432  eldioph2b  43535  diophren  43581  pell1234qrdich  43629  omabs2  44100  iunconnlem2  45684  limcrecl  46386  limclner  46406  icccncfext  46642  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  stoweidlem60  46815  fourierdlem51  46912  fourierdlem77  46938  fourierdlem103  46964  fourierdlem104  46965  smfaddlem1  47518  smfmullem3  47548  chnerlem1  47639  grtriprop  48747  upfval  49995  fuco21  50155