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

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

Proof of Theorem simp121
StepHypRef Expression
1 simp21 1248 . 2 ((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) → 𝜑)
213ad2ant1 1127 1 (((𝜃 ∧ (𝜑𝜓𝜒) ∧ 𝜏) ∧ 𝜂𝜁) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  ax5seglem3  26032  axpasch  26042  exatleN  35213  ps-2b  35291  3atlem1  35292  3atlem2  35293  3atlem4  35295  3atlem5  35296  3atlem6  35297  2llnjaN  35375  4atlem12b  35420  2lplnja  35428  dalempea  35435  dath2  35546  lneq2at  35587  llnexchb2  35678  dalawlem1  35680  osumcllem7N  35771  lhpexle3lem  35820  cdleme26ee  36170  cdlemg34  36522  cdlemg36  36524  cdlemj1  36631  cdlemj2  36632  cdlemk23-3  36712  cdlemk25-3  36714  cdlemk26b-3  36715  cdlemk26-3  36716  cdlemk27-3  36717  cdleml3N  36788
  Copyright terms: Public domain W3C validator