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

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

Proof of Theorem simp131
StepHypRef Expression
1 simp31 1090 . 2 ((𝜃𝜏 ∧ (𝜑𝜓𝜒)) → 𝜑)
213ad2ant1 1075 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂𝜁) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  ax5seglem3  25611  exatleN  33708  3atlem1  33787  3atlem2  33788  3atlem5  33791  2llnjaN  33870  4atlem11b  33912  4atlem12b  33915  lplncvrlvol2  33919  dalemsea  33933  dath2  34041  cdlemblem  34097  dalawlem1  34175  lhpexle3lem  34315  4atexlemex6  34378  cdleme22f2  34653  cdleme22g  34654  cdlemg7aN  34931  cdlemg34  35018  cdlemj1  35127  cdlemk23-3  35208  cdlemk25-3  35210  cdlemk26b-3  35211  cdleml3N  35284
  Copyright terms: Public domain W3C validator