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

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

Proof of Theorem simp122
StepHypRef Expression
1 simp22 1209 . 2 ((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) → 𝜓)
213ad2ant1 1135 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂𝜁) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1089
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 210  df-an 400  df-3an 1091
This theorem is referenced by:  ax5seglem3  27054  axpasch  27064  exatleN  37192  ps-2b  37270  3atlem1  37271  3atlem2  37272  3atlem4  37274  3atlem5  37275  3atlem6  37276  2llnjaN  37354  4atlem12b  37399  2lplnja  37407  dalemqea  37415  dath2  37525  lneq2at  37566  llnexchb2  37657  dalawlem1  37659  lhpexle3lem  37799  cdleme26ee  38148  cdlemg34  38500  cdlemg35  38501  cdlemg36  38502  cdlemj1  38609  cdlemj2  38610  cdlemk23-3  38690  cdlemk25-3  38692  cdlemk26b-3  38693  cdlemk26-3  38694  cdleml3N  38766  iscnrm3llem2  45963
  Copyright terms: Public domain W3C validator