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

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

Proof of Theorem simp122
StepHypRef Expression
1 simp22 1249 . 2 ((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) → 𝜓)
213ad2ant1 1127 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂𝜁) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  ax5seglem3  26025  axpasch  26035  exatleN  35205  ps-2b  35283  3atlem1  35284  3atlem2  35285  3atlem4  35287  3atlem5  35288  3atlem6  35289  2llnjaN  35367  4atlem12b  35412  2lplnja  35420  dalemqea  35428  dath2  35538  lneq2at  35579  llnexchb2  35670  dalawlem1  35672  lhpexle3lem  35812  cdleme26ee  36162  cdlemg34  36514  cdlemg35  36515  cdlemg36  36516  cdlemj1  36623  cdlemj2  36624  cdlemk23-3  36704  cdlemk25-3  36706  cdlemk26b-3  36707  cdlemk26-3  36708  cdleml3N  36780
  Copyright terms: Public domain W3C validator