Theorem simp-5r 805

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 803	. 2 ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
2	1	adantr 480	1 ⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  simp-6r  807  catcocl  16169  catass  16170  monpropd  16220  subccocl  16328  funcco  16354  funcpropd  16383  mhmmnd  17360  pm2mpmhmlem2  20443  neitr  20794  restutopopn  21852  ustuqtop4  21858  utopreg  21866  cfilucfil  22174  psmetutop  22182  dyadmax  23172  tgifscgr  25203  tgcgrxfr  25213  tgbtwnconn1lem3  25269  tgbtwnconn1  25270  legov  25280  legtrd  25284  legso  25294  miriso  25365  perpneq  25409  footex  25413  colperpex  25425  opphllem  25427  midex  25429  opphl  25446  lnopp2hpgb  25455  trgcopyeu  25498  dfcgra2  25521  inaghl  25531  f1otrg  25551  pthdepisspth  26104  clwlkfclwwlk  26371  2sqmo  28980  omndmul2  29043  psgnfzto1stlem  29181  qtophaus  29231  locfinreflem  29235  cmpcref  29245  pstmxmet  29268  lmxrge0  29326  esumcst  29452  omssubadd  29689  signstfvneq0  29975  afsval  30002  matunitlindflem1  32575  heicant  32614  sstotbnd2  32743  eldioph2b  36344  diophren  36395  pell1234qrdich  36443  iunconlem2  38193  limcrecl  38696  limclner  38718  icccncfext  38773  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  stoweidlem60  38953  fourierdlem51  39050  fourierdlem77  39076  fourierdlem103  39102  fourierdlem104  39103  smfaddlem1  39649  smfmullem3  39678  clwlksfclwwlk  41269