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

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

Proof of Theorem simp121
StepHypRef Expression
1 simp21 1208 . 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  27022  axpasch  27032  exatleN  37155  ps-2b  37233  3atlem1  37234  3atlem2  37235  3atlem4  37237  3atlem5  37238  3atlem6  37239  2llnjaN  37317  4atlem12b  37362  2lplnja  37370  dalempea  37377  dath2  37488  lneq2at  37529  llnexchb2  37620  dalawlem1  37622  osumcllem7N  37713  lhpexle3lem  37762  cdleme26ee  38111  cdlemg34  38463  cdlemg36  38465  cdlemj1  38572  cdlemj2  38573  cdlemk23-3  38653  cdlemk25-3  38655  cdlemk26b-3  38656  cdlemk26-3  38657  cdlemk27-3  38658  cdleml3N  38729  iscnrm3llem2  45917
  Copyright terms: Public domain W3C validator