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

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

Proof of Theorem simp123
StepHypRef Expression
1 simp23 1094 . 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  25711  axpasch  25721  exatleN  34170  ps-2b  34248  3atlem1  34249  3atlem2  34250  3atlem4  34252  3atlem5  34253  3atlem6  34254  2llnjaN  34332  2llnjN  34333  4atlem12b  34377  2lplnja  34385  2lplnj  34386  dalemrea  34394  dath2  34503  lneq2at  34544  osumcllem7N  34728  cdleme26ee  35128  cdlemg35  35481  cdlemg36  35482  cdlemj1  35589  cdlemk23-3  35670  cdlemk25-3  35672  cdlemk26b-3  35673  cdlemk27-3  35675  cdlemk28-3  35676  cdleml3N  35746
  Copyright terms: Public domain W3C validator