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

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

Proof of Theorem simp131
StepHypRef Expression
1 simp31 1252 . 2 ((𝜃𝜏 ∧ (𝜑𝜓𝜒)) → 𝜑)
213ad2ant1 1128 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂𝜁) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1072 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 385  df-3an 1074 This theorem is referenced by:  ax5seglem3  26031  exatleN  35211  3atlem1  35290  3atlem2  35291  3atlem5  35294  2llnjaN  35373  4atlem11b  35415  4atlem12b  35418  lplncvrlvol2  35422  dalemsea  35436  dath2  35544  cdlemblem  35600  dalawlem1  35678  lhpexle3lem  35818  4atexlemex6  35881  cdleme22f2  36155  cdleme22g  36156  cdlemg7aN  36433  cdlemg34  36520  cdlemj1  36629  cdlemk23-3  36710  cdlemk25-3  36712  cdlemk26b-3  36713  cdleml3N  36786
 Copyright terms: Public domain W3C validator