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

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

Proof of Theorem simp123
StepHypRef Expression
1 simp23 1200 . 2 ((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) → 𝜒)
213ad2ant1 1125 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂𝜁) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  ax5seglem3  26644  axpasch  26654  exatleN  36420  ps-2b  36498  3atlem1  36499  3atlem2  36500  3atlem4  36502  3atlem5  36503  3atlem6  36504  2llnjaN  36582  2llnjN  36583  4atlem12b  36627  2lplnja  36635  2lplnj  36636  dalemrea  36644  dath2  36753  lneq2at  36794  osumcllem7N  36978  cdleme26ee  37376  cdlemg35  37729  cdlemg36  37730  cdlemj1  37837  cdlemk23-3  37918  cdlemk25-3  37920  cdlemk26b-3  37921  cdlemk27-3  37923  cdlemk28-3  37924  cdleml3N  37994
  Copyright terms: Public domain W3C validator