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  17864  catass  17865  monpropd  17917  subccocl  18025  funcco  18051  funcpropd  18082  chnub  18801  mhmmnd  19279  ghmqusnsg  19501  ghmquskerlem3  19505  omndmul2  20352  rhmqusnsg  21586  rhmpreimaprmidl  21640  ssdifidllem  21645  ssdifidlprm  21647  matunitlindflem1  22999  pm2mpmhmlem2  23142  neitr  23503  restutopopn  24562  ustuqtop4  24568  utopreg  24576  cfilucfil  24883  psmetutop  24891  dyadmax  25924  2sqmo  27769  tgsegconeu  28954  tgifscgr  28976  tgcgrxfr  28986  tgbtwnconn1lem3  29042  tgbtwnconn1  29043  legov  29053  legtrd  29057  legso  29067  miriso  29147  perpneq  29194  footexALT  29198  footex  29201  colperpex  29214  opphllem  29216  midex  29218  opphl  29235  lnopp2hpgb  29246  trgcopyeu  29318  zerocgra  29336  dfcgra2  29343  ragcgra  29348  cgrarag  29349  ragsupplcgra  29350  tgaaddcpbllem1  29354  tgaaddcpbl  29357  inaghl  29369  cgraer  29382  cgrabasimass  29383  angmgmaddcpbl  29395  angmgmaddcl  29396  angmgmaddlid  29397  angmgmaddrid  29398  perpprlng  29433  prlngmolem1  29435  prlngmolem2  29436  prlngmo2  29439  f1otrg  29453  2ndresdju  33290  nn0xmulclb  33409  psgnfzto1stlem  33707  cyc3genpm  33759  elrgspnlem4  33852  rloccring  33878  rlocf1  33881  ricdomn1  33896  dvdsruasso  33986  nsgqusf1olem3  34012  rhmquskerlem  34021  elrspunidl  34024  rhmimaidl  34028  mxidlprm  34041  mxidlirredi  34042  ssmxidl  34045  qsdrngi  34065  qsdrng  34067  1arithidom  34115  1arithufdlem3  34124  r1plmhm  34187  r1pquslmic  34188  mplidomlem  34205  vieta  34258  lbsdiflsp0  34304  fldext2chn  34406  constrconj  34423  constrfin  34424  constrelextdg2  34425  constrfiss  34429  cos9thpiminplylem2  34461  qtophaus  34514  locfinreflem  34518  cmpcref  34528  pstmxmet  34575  lmxrge0  34630  esumcst  34741  omssubadd  34978  signstfvneq0  35247  afsval  35349  heicant  38666  sstotbnd2  38801  primrootscoprmpow  43242  primrootspoweq0  43249  aks6d1c2p2  43262  aks6d1c2lem4  43270  aks6d1c2  43273  unitscyglem3  43340  dffltz  43763  eldioph2b  43867  diophren  43913  pell1234qrdich  43961  omabs2  44427  iunconnlem2  46010  limcrecl  46734  limclner  46754  icccncfext  46990  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  stoweidlem60  47163  fourierdlem51  47260  fourierdlem77  47286  fourierdlem103  47312  fourierdlem104  47313  smfaddlem1  47866  smfmullem3  47896  chnerlem1  47985  grtriprop  49132  upfval  50385  fuco21  50551