Theorem simp-6r 807

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

Assertion

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

Proof of Theorem simp-6r

Step	Hyp	Ref	Expression
1		simp-5r 805	. 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-7r  809  catass  16170  mhmmnd  17360  scmatscm  20138  cfilucfil  22174  istrkgb  25154  istrkge  25156  tgbtwnconn1  25270  legso  25294  footex  25413  opphl  25446  trgcopy  25496  dfcgra2  25521  cgrg3col4  25534  f1otrg  25551  2sqmo  28980  pstmxmet  29268  signstfvneq0  29975  afsval  30002  mblfinlem3  32618  mblfinlem4  32619  iunconlem2  38193  suplesup  38496  limclner  38718  fourierdlem51  39050  hoidmvle  39490  smfmullem3  39678