MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp123 Structured version   Visualization version   GIF version

Theorem simp123 1304
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp123 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂𝜁) → 𝜒)

Proof of Theorem simp123
StepHypRef Expression
1 simp23 1205 . 2 ((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) → 𝜒)
213ad2ant1 1130 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂𝜁) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  ax5seglem3  26725  axpasch  26735  exatleN  36700  ps-2b  36778  3atlem1  36779  3atlem2  36780  3atlem4  36782  3atlem5  36783  3atlem6  36784  2llnjaN  36862  2llnjN  36863  4atlem12b  36907  2lplnja  36915  2lplnj  36916  dalemrea  36924  dath2  37033  lneq2at  37074  osumcllem7N  37258  cdleme26ee  37656  cdlemg35  38009  cdlemg36  38010  cdlemj1  38117  cdlemk23-3  38198  cdlemk25-3  38200  cdlemk26b-3  38201  cdlemk27-3  38203  cdlemk28-3  38204  cdleml3N  38274
  Copyright terms: Public domain W3C validator