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

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

Proof of Theorem simp121
StepHypRef Expression
1 simp21 1200 . 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  26633  axpasch  26643  exatleN  36409  ps-2b  36487  3atlem1  36488  3atlem2  36489  3atlem4  36491  3atlem5  36492  3atlem6  36493  2llnjaN  36571  4atlem12b  36616  2lplnja  36624  dalempea  36631  dath2  36742  lneq2at  36783  llnexchb2  36874  dalawlem1  36876  osumcllem7N  36967  lhpexle3lem  37016  cdleme26ee  37365  cdlemg34  37717  cdlemg36  37719  cdlemj1  37826  cdlemj2  37827  cdlemk23-3  37907  cdlemk25-3  37909  cdlemk26b-3  37910  cdlemk26-3  37911  cdlemk27-3  37912  cdleml3N  37983
  Copyright terms: Public domain W3C validator