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

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

Proof of Theorem simp131
StepHypRef Expression
1 simp31 1095 . 2 ((𝜃𝜏 ∧ (𝜑𝜓𝜒)) → 𝜑)
213ad2ant1 1080 1 (((𝜃𝜏 ∧ (𝜑𝜓𝜒)) ∧ 𝜂𝜁) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  ax5seglem3  25728  exatleN  34205  3atlem1  34284  3atlem2  34285  3atlem5  34288  2llnjaN  34367  4atlem11b  34409  4atlem12b  34412  lplncvrlvol2  34416  dalemsea  34430  dath2  34538  cdlemblem  34594  dalawlem1  34672  lhpexle3lem  34812  4atexlemex6  34875  cdleme22f2  35150  cdleme22g  35151  cdlemg7aN  35428  cdlemg34  35515  cdlemj1  35624  cdlemk23-3  35705  cdlemk25-3  35707  cdlemk26b-3  35708  cdleml3N  35781
  Copyright terms: Public domain W3C validator