Theorem simp-5r 782

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  catcocl  17633  catass  17634  monpropd  17688  subccocl  17799  funcco  17825  funcpropd  17855  mhmmnd  18983  pm2mpmhmlem2  22541  neitr  22904  restutopopn  23963  ustuqtop4  23969  utopreg  23977  cfilucfil  24288  psmetutop  24296  dyadmax  25347  2sqmo  27176  tgifscgr  28026  tgcgrxfr  28036  tgbtwnconn1lem3  28092  tgbtwnconn1  28093  legov  28103  legtrd  28107  legso  28117  miriso  28188  perpneq  28232  footexALT  28236  footex  28239  colperpex  28251  opphllem  28253  midex  28255  opphl  28272  lnopp2hpgb  28281  trgcopyeu  28324  dfcgra2  28348  inaghl  28363  f1otrg  28389  2ndresdju  32141  nn0xmulclb  32251  omndmul2  32500  psgnfzto1stlem  32529  cyc3genpm  32581  dvdsruasso  32764  nsgqusf1olem3  32800  ghmquskerlem3  32805  rhmquskerlem  32817  elrspunidl  32820  rhmimaidl  32824  rhmpreimaprmidl  32844  mxidlprm  32860  mxidlirredi  32861  ssmxidl  32864  qsdrngi  32883  qsdrng  32885  r1plmhm  32955  r1pquslmic  32956  lbsdiflsp0  32999  qtophaus  33114  locfinreflem  33118  cmpcref  33128  pstmxmet  33175  lmxrge0  33230  esumcst  33359  omssubadd  33597  signstfvneq0  33881  afsval  33981  matunitlindflem1  36787  heicant  36826  sstotbnd2  36945  aks6d1c2p2  41263  dffltz  41678  flt4lem7  41703  eldioph2b  41803  diophren  41853  pell1234qrdich  41901  omabs2  42384  iunconnlem2  43998  limcrecl  44643  limclner  44665  icccncfext  44901  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  stoweidlem60  45074  fourierdlem51  45171  fourierdlem77  45197  fourierdlem103  45223  fourierdlem104  45224  smfaddlem1  45777  smfmullem3  45807