Theorem simp-5r 797

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  catcocl  17742  catass  17743  monpropd  17795  subccocl  17903  funcco  17929  funcpropd  17960  chnub  18679  mhmmnd  19131  ghmqusnsg  19353  ghmquskerlem3  19357  omndmul2  20204  rhmqusnsg  21406  rhmpreimaprmidl  21460  ssdifidllem  21465  ssdifidlprm  21467  pm2mpmhmlem2  22957  neitr  23318  restutopopn  24376  ustuqtop4  24382  utopreg  24390  cfilucfil  24697  psmetutop  24705  dyadmax  25738  2sqmo  27582  tgifscgr  28758  tgcgrxfr  28768  tgbtwnconn1lem3  28824  tgbtwnconn1  28825  legov  28835  legtrd  28839  legso  28849  miriso  28928  perpneq  28975  footexALT  28979  footex  28982  colperpex  28995  opphllem  28997  midex  28999  opphl  29016  lnopp2hpgb  29026  trgcopyeu  29098  dfcgra2  29122  ragcgra  29127  cgrarag  29128  ragsupplcgra  29129  inaghl  29143  perpprlng  29181  prlngmolem1  29183  prlngmolem2  29184  prlngmo2  29187  f1otrg  29201  2ndresdju  32975  nn0xmulclb  33097  psgnfzto1stlem  33401  cyc3genpm  33453  elrgspnlem4  33546  rloccring  33572  rlocf1  33575  ricdomn1  33590  dvdsruasso  33679  nsgqusf1olem3  33705  rhmquskerlem  33714  elrspunidl  33717  rhmimaidl  33721  mxidlprm  33734  mxidlirredi  33735  ssmxidl  33738  qsdrngi  33758  qsdrng  33760  1arithidom  33808  1arithufdlem3  33817  r1plmhm  33880  r1pquslmic  33881  mplidomlem  33898  vieta  33951  lbsdiflsp0  33997  fldext2chn  34099  constrconj  34116  constrfin  34117  constrelextdg2  34118  constrfiss  34122  cos9thpiminplylem2  34154  qtophaus  34207  locfinreflem  34211  cmpcref  34221  pstmxmet  34268  lmxrge0  34323  esumcst  34434  omssubadd  34671  signstfvneq0  34940  afsval  35042  matunitlindflem1  38248  heicant  38287  sstotbnd2  38406  primrootscoprmpow  42847  primrootspoweq0  42854  aks6d1c2p2  42867  aks6d1c2lem4  42875  aks6d1c2  42878  unitscyglem3  42945  dffltz  43349  flt4lem7  43374  eldioph2b  43477  diophren  43523  pell1234qrdich  43571  omabs2  44042  iunconnlem2  45626  limcrecl  46328  limclner  46348  icccncfext  46584  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  stoweidlem60  46757  fourierdlem51  46854  fourierdlem77  46880  fourierdlem103  46906  fourierdlem104  46907  smfaddlem1  47460  smfmullem3  47490  chnerlem1  47581  grtriprop  48689  upfval  49937  fuco21  50097