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

Theorem simp123 1122
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp123  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ch )

Proof of Theorem simp123
StepHypRef Expression
1 simp23 1023 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ch )
213ad2ant1 1009 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  ax5seglem3  23322  axpasch  23332  exatleN  33357  ps-2b  33435  3atlem1  33436  3atlem2  33437  3atlem4  33439  3atlem5  33440  3atlem6  33441  2llnjaN  33519  2llnjN  33520  4atlem12b  33564  2lplnja  33572  2lplnj  33573  dalemrea  33581  dath2  33690  lneq2at  33731  osumcllem7N  33915  cdleme26ee  34313  cdlemg35  34666  cdlemg36  34667  cdlemj1  34774  cdlemk23-3  34855  cdlemk25-3  34857  cdlemk26b-3  34858  cdlemk27-3  34860  cdlemk28-3  34861  cdleml3N  34931
  Copyright terms: Public domain W3C validator