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

Theorem simp123 1133
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 1034 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ch )
213ad2ant1 1020 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 976
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 187  df-an 371  df-3an 978
This theorem is referenced by:  ax5seglem3  24663  axpasch  24673  exatleN  32434  ps-2b  32512  3atlem1  32513  3atlem2  32514  3atlem4  32516  3atlem5  32517  3atlem6  32518  2llnjaN  32596  2llnjN  32597  4atlem12b  32641  2lplnja  32649  2lplnj  32650  dalemrea  32658  dath2  32767  lneq2at  32808  osumcllem7N  32992  cdleme26ee  33392  cdlemg35  33745  cdlemg36  33746  cdlemj1  33853  cdlemk23-3  33934  cdlemk25-3  33936  cdlemk26b-3  33937  cdlemk27-3  33939  cdlemk28-3  33940  cdleml3N  34010
  Copyright terms: Public domain W3C validator