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  17839  catass  17840  monpropd  17892  subccocl  18000  funcco  18026  funcpropd  18057  chnub  18776  mhmmnd  19254  ghmqusnsg  19476  ghmquskerlem3  19480  omndmul2  20327  rhmqusnsg  21561  rhmpreimaprmidl  21615  ssdifidllem  21620  ssdifidlprm  21622  matunitlindflem1  22974  pm2mpmhmlem2  23117  neitr  23478  restutopopn  24537  ustuqtop4  24543  utopreg  24551  cfilucfil  24858  psmetutop  24866  dyadmax  25899  2sqmo  27746  flt4lem7  27971  tgsegconeu  28931  tgifscgr  28953  tgcgrxfr  28963  tgbtwnconn1lem3  29019  tgbtwnconn1  29020  legov  29030  legtrd  29034  legso  29044  miriso  29124  perpneq  29171  footexALT  29175  footex  29178  colperpex  29191  opphllem  29193  midex  29195  opphl  29212  lnopp2hpgb  29223  trgcopyeu  29295  zerocgra  29313  dfcgra2  29320  ragcgra  29325  cgrarag  29326  ragsupplcgra  29327  tgaaddcpbllem1  29331  tgaaddcpbl  29334  inaghl  29346  cgraer  29359  cgrabasimass  29360  angmgmaddcpbl  29372  angmgmaddcl  29373  angmgmaddlid  29374  angmgmaddrid  29375  perpprlng  29410  prlngmolem1  29412  prlngmolem2  29413  prlngmo2  29416  f1otrg  29430  2ndresdju  33225  nn0xmulclb  33345  psgnfzto1stlem  33643  cyc3genpm  33695  elrgspnlem4  33788  rloccring  33814  rlocf1  33817  ricdomn1  33832  dvdsruasso  33922  nsgqusf1olem3  33948  rhmquskerlem  33957  elrspunidl  33960  rhmimaidl  33964  mxidlprm  33977  mxidlirredi  33978  ssmxidl  33981  qsdrngi  34001  qsdrng  34003  1arithidom  34051  1arithufdlem3  34060  r1plmhm  34123  r1pquslmic  34124  mplidomlem  34141  vieta  34194  lbsdiflsp0  34240  fldext2chn  34342  constrconj  34359  constrfin  34360  constrelextdg2  34361  constrfiss  34365  cos9thpiminplylem2  34397  qtophaus  34450  locfinreflem  34454  cmpcref  34464  pstmxmet  34511  lmxrge0  34566  esumcst  34677  omssubadd  34915  signstfvneq0  35184  afsval  35286  heicant  38541  sstotbnd2  38676  primrootscoprmpow  43117  primrootspoweq0  43124  aks6d1c2p2  43137  aks6d1c2lem4  43145  aks6d1c2  43148  unitscyglem3  43215  dffltz  43624  eldioph2b  43727  diophren  43773  pell1234qrdich  43821  omabs2  44292  iunconnlem2  45876  limcrecl  46585  limclner  46605  icccncfext  46841  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  stoweidlem60  47014  fourierdlem51  47111  fourierdlem77  47137  fourierdlem103  47163  fourierdlem104  47164  smfaddlem1  47717  smfmullem3  47747  chnerlem1  47836  grtriprop  48983  upfval  50228  fuco21  50388