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

Theorem simp123 1092
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 993 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ch )
213ad2ant1 979 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  ax5seglem3  25872  axpasch  25882  exatleN  30263  ps-2b  30341  3atlem1  30342  3atlem2  30343  3atlem4  30345  3atlem5  30346  3atlem6  30347  2llnjaN  30425  2llnjN  30426  4atlem12b  30470  2lplnja  30478  2lplnj  30479  dalemrea  30487  dath2  30596  lneq2at  30637  osumcllem7N  30821  cdleme26ee  31219  cdlemg35  31572  cdlemg36  31573  cdlemj1  31680  cdlemk23-3  31761  cdlemk25-3  31763  cdlemk26b-3  31764  cdlemk27-3  31766  cdlemk28-3  31767  cdleml3N  31837
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator