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

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

Proof of Theorem simp133
StepHypRef Expression
1 simp33 1097 . 2 ((𝜃𝜏 ∧ (𝜑𝜓𝜒)) → 𝜒)
213ad2ant1 1080 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂𝜁) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  tsmsxp  21868  ax5seglem3  25711  exatleN  34170  3atlem1  34249  3atlem2  34250  3atlem6  34254  4atlem11b  34374  4atlem12b  34377  lplncvrlvol2  34381  dalemuea  34397  dath2  34503  4atexlemex6  34840  cdleme22f2  35115  cdleme22g  35116  cdlemg7aN  35393  cdlemg31c  35467  cdlemg36  35482  cdlemj1  35589  cdlemj2  35590  cdlemk23-3  35670  cdlemk26b-3  35673
  Copyright terms: Public domain W3C validator