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  17779  catass  17780  monpropd  17832  subccocl  17940  funcco  17966  funcpropd  17997  chnub  18716  mhmmnd  19193  ghmqusnsg  19415  ghmquskerlem3  19419  omndmul2  20266  rhmqusnsg  21494  rhmpreimaprmidl  21548  ssdifidllem  21553  ssdifidlprm  21555  matunitlindflem1  22907  pm2mpmhmlem2  23050  neitr  23411  restutopopn  24470  ustuqtop4  24476  utopreg  24484  cfilucfil  24791  psmetutop  24799  dyadmax  25832  2sqmo  27681  tgsegconeu  28836  tgifscgr  28858  tgcgrxfr  28868  tgbtwnconn1lem3  28924  tgbtwnconn1  28925  legov  28935  legtrd  28939  legso  28949  miriso  29029  perpneq  29076  footexALT  29080  footex  29083  colperpex  29096  opphllem  29098  midex  29100  opphl  29117  lnopp2hpgb  29128  trgcopyeu  29200  zerocgra  29218  dfcgra2  29225  ragcgra  29230  cgrarag  29231  ragsupplcgra  29232  tgaaddcpbllem1  29236  tgaaddcpbl  29239  inaghl  29251  cgraer  29264  cgrabasimass  29265  angmgmaddcpbl  29277  angmgmaddcl  29278  angmgmaddlid  29279  angmgmaddrid  29280  perpprlng  29315  prlngmolem1  29317  prlngmolem2  29318  prlngmo2  29321  f1otrg  29335  2ndresdju  33130  nn0xmulclb  33250  psgnfzto1stlem  33548  cyc3genpm  33600  elrgspnlem4  33693  rloccring  33719  rlocf1  33722  ricdomn1  33737  dvdsruasso  33826  nsgqusf1olem3  33852  rhmquskerlem  33861  elrspunidl  33864  rhmimaidl  33868  mxidlprm  33881  mxidlirredi  33882  ssmxidl  33885  qsdrngi  33905  qsdrng  33907  1arithidom  33955  1arithufdlem3  33964  r1plmhm  34027  r1pquslmic  34028  mplidomlem  34045  vieta  34098  lbsdiflsp0  34144  fldext2chn  34246  constrconj  34263  constrfin  34264  constrelextdg2  34265  constrfiss  34269  cos9thpiminplylem2  34301  qtophaus  34354  locfinreflem  34358  cmpcref  34368  pstmxmet  34415  lmxrge0  34470  esumcst  34581  omssubadd  34819  signstfvneq0  35088  afsval  35190  heicant  38412  sstotbnd2  38532  primrootscoprmpow  42973  primrootspoweq0  42980  aks6d1c2p2  42993  aks6d1c2lem4  43001  aks6d1c2  43004  unitscyglem3  43071  dffltz  43488  flt4lem7  43513  eldioph2b  43616  diophren  43662  pell1234qrdich  43710  omabs2  44181  iunconnlem2  45765  limcrecl  46467  limclner  46487  icccncfext  46723  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  stoweidlem60  46896  fourierdlem51  46993  fourierdlem77  47019  fourierdlem103  47045  fourierdlem104  47046  smfaddlem1  47599  smfmullem3  47629  chnerlem1  47718  grtriprop  48865  upfval  50110  fuco21  50270