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

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

Proof of Theorem simp122
StepHypRef Expression
1 simp22 1088 . 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  dalemqea  33931  dath2  34041  lneq2at  34082  llnexchb2  34173  dalawlem1  34175  lhpexle3lem  34315  cdleme26ee  34666  cdlemg34  35018  cdlemg35  35019  cdlemg36  35020  cdlemj1  35127  cdlemj2  35128  cdlemk23-3  35208  cdlemk25-3  35210  cdlemk26b-3  35211  cdlemk26-3  35212  cdleml3N  35284
 Copyright terms: Public domain W3C validator