Theorem simp-5r 809

Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)

Assertion

Ref	Expression
simp-5r	⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem simp-5r

Step	Hyp	Ref	Expression
1		simp-4r 807	. 2 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
2	1	adantr 481	1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  simp-6r  811  catcocl  16346  catass  16347  monpropd  16397  subccocl  16505  funcco  16531  funcpropd  16560  mhmmnd  17537  pm2mpmhmlem2  20624  neitr  20984  restutopopn  22042  ustuqtop4  22048  utopreg  22056  cfilucfil  22364  psmetutop  22372  dyadmax  23366  tgifscgr  25403  tgcgrxfr  25413  tgbtwnconn1lem3  25469  tgbtwnconn1  25470  legov  25480  legtrd  25484  legso  25494  miriso  25565  perpneq  25609  footex  25613  colperpex  25625  opphllem  25627  midex  25629  opphl  25646  lnopp2hpgb  25655  trgcopyeu  25698  dfcgra2  25721  inaghl  25731  f1otrg  25751  clwlksfclwwlk  26962  2sqmo  29649  omndmul2  29712  psgnfzto1stlem  29850  qtophaus  29903  locfinreflem  29907  cmpcref  29917  pstmxmet  29940  lmxrge0  29998  esumcst  30125  omssubadd  30362  signstfvneq0  30649  afsval  30749  matunitlindflem1  33405  heicant  33444  sstotbnd2  33573  eldioph2b  37326  diophren  37377  pell1234qrdich  37425  iunconnlem2  39171  limcrecl  39861  limclner  39883  icccncfext  40100  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  stoweidlem60  40277  fourierdlem51  40374  fourierdlem77  40400  fourierdlem103  40426  fourierdlem104  40427  smfaddlem1  40971  smfmullem3  41000