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

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

Proof of Theorem simp131
StepHypRef Expression
1 simp31 1251 . 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:  ax5seglem3  26032  exatleN  35212  3atlem1  35291  3atlem2  35292  3atlem5  35295  2llnjaN  35374  4atlem11b  35416  4atlem12b  35419  lplncvrlvol2  35423  dalemsea  35437  dath2  35545  cdlemblem  35601  dalawlem1  35679  lhpexle3lem  35819  4atexlemex6  35882  cdleme22f2  36156  cdleme22g  36157  cdlemg7aN  36434  cdlemg34  36521  cdlemj1  36630  cdlemk23-3  36711  cdlemk25-3  36713  cdlemk26b-3  36714  cdleml3N  36787
  Copyright terms: Public domain W3C validator