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

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

Proof of Theorem simp133
StepHypRef Expression
1 simp33 1253 . 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:  tsmsxp  22178  ax5seglem3  26032  exatleN  35212  3atlem1  35291  3atlem2  35292  3atlem6  35296  4atlem11b  35416  4atlem12b  35419  lplncvrlvol2  35423  dalemuea  35439  dath2  35545  4atexlemex6  35882  cdleme22f2  36156  cdleme22g  36157  cdlemg7aN  36434  cdlemg31c  36508  cdlemg36  36523  cdlemj1  36630  cdlemj2  36631  cdlemk23-3  36711  cdlemk26b-3  36714
  Copyright terms: Public domain W3C validator