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  17588  catass  17589  monpropd  17641  subccocl  17749  funcco  17775  funcpropd  17806  chnub  18525  mhmmnd  18974  ghmqusnsg  19192  ghmquskerlem3  19196  omndmul2  20043  rhmqusnsg  21220  pm2mpmhmlem2  22732  neitr  23093  restutopopn  24151  ustuqtop4  24157  utopreg  24165  cfilucfil  24472  psmetutop  24480  dyadmax  25524  2sqmo  27373  tgifscgr  28484  tgcgrxfr  28494  tgbtwnconn1lem3  28550  tgbtwnconn1  28551  legov  28561  legtrd  28565  legso  28575  miriso  28646  perpneq  28690  footexALT  28694  footex  28697  colperpex  28709  opphllem  28711  midex  28713  opphl  28730  lnopp2hpgb  28739  trgcopyeu  28782  dfcgra2  28806  inaghl  28821  f1otrg  28847  2ndresdju  32626  nn0xmulclb  32749  psgnfzto1stlem  33064  cyc3genpm  33116  elrgspnlem4  33207  rloccring  33232  rlocf1  33235  dvdsruasso  33345  nsgqusf1olem3  33375  rhmquskerlem  33385  elrspunidl  33388  rhmimaidl  33392  rhmpreimaprmidl  33411  ssdifidllem  33416  ssdifidlprm  33418  mxidlprm  33430  mxidlirredi  33431  ssmxidl  33434  qsdrngi  33455  qsdrng  33457  1arithidom  33497  1arithufdlem3  33506  r1plmhm  33565  r1pquslmic  33566  lbsdiflsp0  33634  fldext2chn  33736  constrconj  33753  constrfin  33754  constrelextdg2  33755  constrfiss  33759  cos9thpiminplylem2  33791  qtophaus  33844  locfinreflem  33848  cmpcref  33858  pstmxmet  33905  lmxrge0  33960  esumcst  34071  omssubadd  34308  signstfvneq0  34580  afsval  34679  matunitlindflem1  37655  heicant  37694  sstotbnd2  37813  primrootscoprmpow  42131  primrootspoweq0  42138  aks6d1c2p2  42151  aks6d1c2lem4  42159  aks6d1c2  42162  unitscyglem3  42229  dffltz  42666  flt4lem7  42691  eldioph2b  42795  diophren  42845  pell1234qrdich  42893  omabs2  43364  iunconnlem2  44966  limcrecl  45668  limclner  45688  icccncfext  45924  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  stoweidlem60  46097  fourierdlem51  46194  fourierdlem77  46220  fourierdlem103  46246  fourierdlem104  46247  smfaddlem1  46800  smfmullem3  46830  grtriprop  47971  upfval  49207  fuco21  49367