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

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

Proof of Theorem simp122
StepHypRef Expression
1 simp22 1093 . 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  25724  axpasch  25734  exatleN  34197  ps-2b  34275  3atlem1  34276  3atlem2  34277  3atlem4  34279  3atlem5  34280  3atlem6  34281  2llnjaN  34359  4atlem12b  34404  2lplnja  34412  dalemqea  34420  dath2  34530  lneq2at  34571  llnexchb2  34662  dalawlem1  34664  lhpexle3lem  34804  cdleme26ee  35155  cdlemg34  35507  cdlemg35  35508  cdlemg36  35509  cdlemj1  35616  cdlemj2  35617  cdlemk23-3  35697  cdlemk25-3  35699  cdlemk26b-3  35700  cdlemk26-3  35701  cdleml3N  35773
  Copyright terms: Public domain W3C validator