Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp-6r Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 simp-5r 805 . 2 ((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓)
21adantr 480 1 (((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator