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

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

Proof of Theorem simp131
StepHypRef Expression
1 simp31 1203 . 2 ((𝜃𝜏 ∧ (𝜑𝜓𝜒)) → 𝜑)
213ad2ant1 1127 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂𝜁) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  ax5seglem3  26634  exatleN  36410  3atlem1  36489  3atlem2  36490  3atlem5  36493  2llnjaN  36572  4atlem11b  36614  4atlem12b  36617  lplncvrlvol2  36621  dalemsea  36635  dath2  36743  cdlemblem  36799  dalawlem1  36877  lhpexle3lem  37017  4atexlemex6  37080  cdleme22f2  37353  cdleme22g  37354  cdlemg7aN  37631  cdlemg34  37718  cdlemj1  37827  cdlemk23-3  37908  cdlemk25-3  37910  cdlemk26b-3  37911  cdleml3N  37984
  Copyright terms: Public domain W3C validator