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

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

Proof of Theorem simp131
StepHypRef Expression
1 simp31 1201 . 2 ((𝜃𝜏 ∧ (𝜑𝜓𝜒)) → 𝜑)
213ad2ant1 1125 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂𝜁) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 1081
This theorem is referenced by:  ax5seglem3  26644  exatleN  36420  3atlem1  36499  3atlem2  36500  3atlem5  36503  2llnjaN  36582  4atlem11b  36624  4atlem12b  36627  lplncvrlvol2  36631  dalemsea  36645  dath2  36753  cdlemblem  36809  dalawlem1  36887  lhpexle3lem  37027  4atexlemex6  37090  cdleme22f2  37363  cdleme22g  37364  cdlemg7aN  37641  cdlemg34  37728  cdlemj1  37837  cdlemk23-3  37918  cdlemk25-3  37920  cdlemk26b-3  37921  cdleml3N  37994
  Copyright terms: Public domain W3C validator