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

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

Proof of Theorem simp132
StepHypRef Expression
1 simp32 1208 . 2 ((𝜃𝜏 ∧ (𝜑𝜓𝜒)) → 𝜓)
213ad2ant1 1131 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂𝜁) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1085
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 395  df-3an 1087
This theorem is referenced by:  ax5seglem3  28456  3atlem1  38657  3atlem2  38658  3atlem5  38661  2llnjaN  38740  4atlem11b  38782  4atlem12b  38785  lplncvrlvol2  38789  dalemtea  38804  dath2  38911  cdlemblem  38967  dalawlem1  39045  lhpexle3lem  39185  4atexlemex6  39248  cdleme22f2  39521  cdleme22g  39522  cdlemg7aN  39799  cdlemg34  39886  cdlemj1  39995  cdlemk23-3  40076  cdlemk25-3  40078  cdlemk26b-3  40079
  Copyright terms: Public domain W3C validator