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

Theorem simp123 1130
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 1031 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ch )
213ad2ant1 1017 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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 975
This theorem is referenced by:  ax5seglem3  23910  axpasch  23920  exatleN  34200  ps-2b  34278  3atlem1  34279  3atlem2  34280  3atlem4  34282  3atlem5  34283  3atlem6  34284  2llnjaN  34362  2llnjN  34363  4atlem12b  34407  2lplnja  34415  2lplnj  34416  dalemrea  34424  dath2  34533  lneq2at  34574  osumcllem7N  34758  cdleme26ee  35156  cdlemg35  35509  cdlemg36  35510  cdlemj1  35617  cdlemk23-3  35698  cdlemk25-3  35700  cdlemk26b-3  35701  cdlemk27-3  35703  cdlemk28-3  35704  cdleml3N  35774
  Copyright terms: Public domain W3C validator