MPE Home 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  16119  mhmmnd  17309  scmatscm  20086  cfilucfil  22122  istrkgb  25099  istrkge  25101  tgbtwnconn1  25216  legso  25240  footex  25359  opphl  25392  trgcopy  25442  dfcgra2  25467  cgrg3col4  25480  f1otrg  25497  2sqmo  28774  pstmxmet  29062  signstfvneq0  29769  afsval  29796  mblfinlem3  32412  mblfinlem4  32413  iunconlem2  37987  suplesup  38290  limclner  38512  fourierdlem51  38844  hoidmvle  39284  smfmullem3  39472
  Copyright terms: Public domain W3C validator