Theorem simp-5l 808

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

Assertion

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

Proof of Theorem simp-5l

Step	Hyp	Ref	Expression
1		simp-4l 806	. 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-6l  810  mhmmnd  17537  neiptopnei  20936  neitx  21410  ustex3sym  22021  restutop  22041  ustuqtop4  22048  utopreg  22056  xrge0tsms  22637  f1otrg  25751  xrge0tsmsd  29785  pstmxmet  29940  esumfsup  30132  esum2dlem  30154  esum2d  30155  omssubadd  30362  eulerpartlemgvv  30438  matunitlindflem2  33406  eldioph2  37325  limcrecl  39861  icccncfext  40100  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  stoweidlem60  40277  fourierdlem77  40400  fourierdlem80  40403  fourierdlem103  40426  fourierdlem104  40427  etransclem35  40486