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

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

Proof of Theorem simp133
StepHypRef Expression
1 simp33 1205 . 2 ((𝜃𝜏 ∧ (𝜑𝜓𝜒)) → 𝜒)
213ad2ant1 1127 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂𝜁) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1081 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 208  df-an 397  df-3an 1083 This theorem is referenced by:  tsmsxp  22680  ax5seglem3  26633  exatleN  36409  3atlem1  36488  3atlem2  36489  3atlem6  36493  4atlem11b  36613  4atlem12b  36616  lplncvrlvol2  36620  dalemuea  36636  dath2  36742  4atexlemex6  37079  cdleme22f2  37352  cdleme22g  37353  cdlemg7aN  37630  cdlemg31c  37704  cdlemg36  37719  cdlemj1  37826  cdlemj2  37827  cdlemk23-3  37907  cdlemk26b-3  37910
 Copyright terms: Public domain W3C validator