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

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

Proof of Theorem simp123
StepHypRef Expression
1 simp23 1251 . 2 ((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) → 𝜒)
213ad2ant1 1128 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂𝜁) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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  df-3an 1074
This theorem is referenced by:  ax5seglem3  26031  axpasch  26041  exatleN  35211  ps-2b  35289  3atlem1  35290  3atlem2  35291  3atlem4  35293  3atlem5  35294  3atlem6  35295  2llnjaN  35373  2llnjN  35374  4atlem12b  35418  2lplnja  35426  2lplnj  35427  dalemrea  35435  dath2  35544  lneq2at  35585  osumcllem7N  35769  cdleme26ee  36168  cdlemg35  36521  cdlemg36  36522  cdlemj1  36629  cdlemk23-3  36710  cdlemk25-3  36712  cdlemk26b-3  36713  cdlemk27-3  36715  cdlemk28-3  36716  cdleml3N  36786
  Copyright terms: Public domain W3C validator