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

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

Proof of Theorem simp121
StepHypRef Expression
1 simp21 1264 . 2 ((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) → 𝜑)
213ad2ant1 1164 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂𝜁) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1108
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 199  df-an 386  df-3an 1110
This theorem is referenced by:  ax5seglem3  26168  axpasch  26178  exatleN  35425  ps-2b  35503  3atlem1  35504  3atlem2  35505  3atlem4  35507  3atlem5  35508  3atlem6  35509  2llnjaN  35587  4atlem12b  35632  2lplnja  35640  dalempea  35647  dath2  35758  lneq2at  35799  llnexchb2  35890  dalawlem1  35892  osumcllem7N  35983  lhpexle3lem  36032  cdleme26ee  36381  cdlemg34  36733  cdlemg36  36735  cdlemj1  36842  cdlemj2  36843  cdlemk23-3  36923  cdlemk25-3  36925  cdlemk26b-3  36926  cdlemk26-3  36927  cdlemk27-3  36928  cdleml3N  36999
  Copyright terms: Public domain W3C validator