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

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

Proof of Theorem simp132
StepHypRef Expression
1 simp32 1096 . 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:  ax5seglem3  25706  3atlem1  34235  3atlem2  34236  3atlem5  34239  2llnjaN  34318  4atlem11b  34360  4atlem12b  34363  lplncvrlvol2  34367  dalemtea  34382  dath2  34489  cdlemblem  34545  dalawlem1  34623  lhpexle3lem  34763  4atexlemex6  34826  cdleme22f2  35101  cdleme22g  35102  cdlemg7aN  35379  cdlemg34  35466  cdlemj1  35575  cdlemk23-3  35656  cdlemk25-3  35658  cdlemk26b-3  35659
  Copyright terms: Public domain W3C validator