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

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

Proof of Theorem simp123
StepHypRef Expression
1 simp23 1209 . 2 ((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) → 𝜒)
213ad2ant1 1134 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂𝜁) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  ax5seglem3  28220  axpasch  28230  exatleN  38323  ps-2b  38401  3atlem1  38402  3atlem2  38403  3atlem4  38405  3atlem5  38406  3atlem6  38407  2llnjaN  38485  2llnjN  38486  4atlem12b  38530  2lplnja  38538  2lplnj  38539  dalemrea  38547  dath2  38656  lneq2at  38697  osumcllem7N  38881  cdleme26ee  39279  cdlemg35  39632  cdlemg36  39633  cdlemj1  39740  cdlemk23-3  39821  cdlemk25-3  39823  cdlemk26b-3  39824  cdlemk27-3  39826  cdlemk28-3  39827  cdleml3N  39897  iscnrm3llem2  47631
  Copyright terms: Public domain W3C validator