Theorem simp-5r 795

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 745	1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  catcocl  17700  catass  17701  monpropd  17753  subccocl  17861  funcco  17887  funcpropd  17918  chnub  18637  mhmmnd  19089  ghmqusnsg  19305  ghmquskerlem3  19309  omndmul2  20156  rhmqusnsg  21335  pm2mpmhmlem2  22859  neitr  23220  restutopopn  24278  ustuqtop4  24284  utopreg  24292  cfilucfil  24599  psmetutop  24607  dyadmax  25640  2sqmo  27478  tgifscgr  28654  tgcgrxfr  28664  tgbtwnconn1lem3  28720  tgbtwnconn1  28721  legov  28731  legtrd  28735  legso  28745  miriso  28816  perpneq  28860  footexALT  28864  footex  28867  colperpex  28879  opphllem  28881  midex  28883  opphl  28900  lnopp2hpgb  28909  trgcopyeu  28952  dfcgra2  28976  inaghl  28991  f1otrg  29017  2ndresdju  32801  nn0xmulclb  32923  psgnfzto1stlem  33241  cyc3genpm  33293  elrgspnlem4  33387  rloccring  33413  rlocf1  33416  ricdomn1  33434  dvdsruasso  33532  nsgqusf1olem3  33562  rhmquskerlem  33572  elrspunidl  33575  rhmimaidl  33579  rhmpreimaprmidl  33599  ssdifidllem  33604  ssdifidlprm  33606  mxidlprm  33619  mxidlirredi  33620  ssmxidl  33623  qsdrngi  33644  qsdrng  33646  1arithidom  33694  1arithufdlem3  33703  r1plmhm  33767  r1pquslmic  33768  mplidomlem  33785  vieta  33838  lbsdiflsp0  33884  fldext2chn  33986  constrconj  34003  constrfin  34004  constrelextdg2  34005  constrfiss  34009  cos9thpiminplylem2  34041  qtophaus  34094  locfinreflem  34098  cmpcref  34108  pstmxmet  34155  lmxrge0  34210  esumcst  34321  omssubadd  34558  signstfvneq0  34830  afsval  34932  matunitlindflem1  38079  heicant  38118  sstotbnd2  38237  primrootscoprmpow  42680  primrootspoweq0  42687  aks6d1c2p2  42700  aks6d1c2lem4  42708  aks6d1c2  42711  unitscyglem3  42778  dffltz  43180  flt4lem7  43205  eldioph2b  43308  diophren  43354  pell1234qrdich  43402  omabs2  43873  iunconnlem2  45474  limcrecl  46169  limclner  46189  icccncfext  46425  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  stoweidlem60  46598  fourierdlem51  46695  fourierdlem77  46721  fourierdlem103  46747  fourierdlem104  46748  smfaddlem1  47301  smfmullem3  47331  chnerlem1  47422  grtriprop  48527  upfval  49761  fuco21  49921