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  28169  axpasch  28179  exatleN  38213  ps-2b  38291  3atlem1  38292  3atlem2  38293  3atlem4  38295  3atlem5  38296  3atlem6  38297  2llnjaN  38375  2llnjN  38376  4atlem12b  38420  2lplnja  38428  2lplnj  38429  dalemrea  38437  dath2  38546  lneq2at  38587  osumcllem7N  38771  cdleme26ee  39169  cdlemg35  39522  cdlemg36  39523  cdlemj1  39630  cdlemk23-3  39711  cdlemk25-3  39713  cdlemk26b-3  39714  cdlemk27-3  39716  cdlemk28-3  39717  cdleml3N  39787  iscnrm3llem2  47485
  Copyright terms: Public domain W3C validator