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

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

Proof of Theorem simp121
StepHypRef Expression
1 simp21 1087 . 2 ((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) → 𝜑)
213ad2ant1 1075 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂𝜁) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  ax5seglem3  25611  axpasch  25621  exatleN  33708  ps-2b  33786  3atlem1  33787  3atlem2  33788  3atlem4  33790  3atlem5  33791  3atlem6  33792  2llnjaN  33870  4atlem12b  33915  2lplnja  33923  dalempea  33930  dath2  34041  lneq2at  34082  llnexchb2  34173  dalawlem1  34175  osumcllem7N  34266  lhpexle3lem  34315  cdleme26ee  34666  cdlemg34  35018  cdlemg36  35020  cdlemj1  35127  cdlemj2  35128  cdlemk23-3  35208  cdlemk25-3  35210  cdlemk26b-3  35211  cdlemk26-3  35212  cdlemk27-3  35213  cdleml3N  35284
  Copyright terms: Public domain W3C validator