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

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

Proof of Theorem simp121
StepHypRef Expression
1 simp21 1092 . 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  25718  axpasch  25728  exatleN  34191  ps-2b  34269  3atlem1  34270  3atlem2  34271  3atlem4  34273  3atlem5  34274  3atlem6  34275  2llnjaN  34353  4atlem12b  34398  2lplnja  34406  dalempea  34413  dath2  34524  lneq2at  34565  llnexchb2  34656  dalawlem1  34658  osumcllem7N  34749  lhpexle3lem  34798  cdleme26ee  35149  cdlemg34  35501  cdlemg36  35503  cdlemj1  35610  cdlemj2  35611  cdlemk23-3  35691  cdlemk25-3  35693  cdlemk26b-3  35694  cdlemk26-3  35695  cdlemk27-3  35696  cdleml3N  35767
  Copyright terms: Public domain W3C validator