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

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

Proof of Theorem simp123
StepHypRef Expression
1 simp23 1250 . 2 ((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) → 𝜒)
213ad2ant1 1127 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂𝜁) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  ax5seglem3  26032  axpasch  26042  exatleN  35212  ps-2b  35290  3atlem1  35291  3atlem2  35292  3atlem4  35294  3atlem5  35295  3atlem6  35296  2llnjaN  35374  2llnjN  35375  4atlem12b  35419  2lplnja  35427  2lplnj  35428  dalemrea  35436  dath2  35545  lneq2at  35586  osumcllem7N  35770  cdleme26ee  36169  cdlemg35  36522  cdlemg36  36523  cdlemj1  36630  cdlemk23-3  36711  cdlemk25-3  36713  cdlemk26b-3  36714  cdlemk27-3  36716  cdlemk28-3  36717  cdleml3N  36787
  Copyright terms: Public domain W3C validator