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

Theorem simp-6r 835
 Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.)
Assertion
Ref Expression
simp-6r (((((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓)

Proof of Theorem simp-6r
StepHypRef Expression
1 simpr 479 . 2 ((𝜑𝜓) → 𝜓)
21ad5antr 775 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 197  df-an 385 This theorem is referenced by:  simp-7rOLD  840  catass  16568  mhmmnd  17758  scmatscm  20541  cfilucfil  22585  istrkgb  25574  istrkge  25576  tgbtwnconn1  25690  legso  25714  footex  25833  opphl  25866  trgcopy  25916  dfcgra2  25941  cgrg3col4  25954  f1otrg  25971  2sqmo  29979  pstmxmet  30270  signstfvneq0  30979  afsval  31079  mblfinlem3  33779  mblfinlem4  33780  iunconnlem2  39688  suplesup  40071  limclner  40404  fourierdlem51  40895  hoidmvle  41338  smfmullem3  41524
 Copyright terms: Public domain W3C validator