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

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

Proof of Theorem simp122
StepHypRef Expression
1 simp22 1203 . 2 ((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) → 𝜓)
213ad2ant1 1129 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂𝜁) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1083
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 209  df-an 399  df-3an 1085
This theorem is referenced by:  ax5seglem3  26716  axpasch  26726  exatleN  36539  ps-2b  36617  3atlem1  36618  3atlem2  36619  3atlem4  36621  3atlem5  36622  3atlem6  36623  2llnjaN  36701  4atlem12b  36746  2lplnja  36754  dalemqea  36762  dath2  36872  lneq2at  36913  llnexchb2  37004  dalawlem1  37006  lhpexle3lem  37146  cdleme26ee  37495  cdlemg34  37847  cdlemg35  37848  cdlemg36  37849  cdlemj1  37956  cdlemj2  37957  cdlemk23-3  38037  cdlemk25-3  38039  cdlemk26b-3  38040  cdlemk26-3  38041  cdleml3N  38113
  Copyright terms: Public domain W3C validator