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

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

Proof of Theorem simp122
StepHypRef Expression
1 simp22 1207 . 2 ((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) → 𝜓)
213ad2ant1 1133 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂𝜁) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1086
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 207  df-an 396  df-3an 1088
This theorem is referenced by:  ax5seglem3  28947  axpasch  28957  exatleN  39407  ps-2b  39485  3atlem1  39486  3atlem2  39487  3atlem4  39489  3atlem5  39490  3atlem6  39491  2llnjaN  39569  4atlem12b  39614  2lplnja  39622  dalemqea  39630  dath2  39740  lneq2at  39781  llnexchb2  39872  dalawlem1  39874  lhpexle3lem  40014  cdleme26ee  40363  cdlemg34  40715  cdlemg35  40716  cdlemg36  40717  cdlemj1  40824  cdlemj2  40825  cdlemk23-3  40905  cdlemk25-3  40907  cdlemk26b-3  40908  cdlemk26-3  40909  cdleml3N  40981  iscnrm3llem2  48854
  Copyright terms: Public domain W3C validator