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

Theorem simp123 1140
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 1041 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ch )
213ad2ant1 1027 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  ax5seglem3  24953  axpasch  24963  exatleN  32894  ps-2b  32972  3atlem1  32973  3atlem2  32974  3atlem4  32976  3atlem5  32977  3atlem6  32978  2llnjaN  33056  2llnjN  33057  4atlem12b  33101  2lplnja  33109  2lplnj  33110  dalemrea  33118  dath2  33227  lneq2at  33268  osumcllem7N  33452  cdleme26ee  33852  cdlemg35  34205  cdlemg36  34206  cdlemj1  34313  cdlemk23-3  34394  cdlemk25-3  34396  cdlemk26b-3  34397  cdlemk27-3  34399  cdlemk28-3  34400  cdleml3N  34470
  Copyright terms: Public domain W3C validator