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

Theorem simp123 1089
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 990 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ch )
213ad2ant1 976 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  ax5seglem3  24559  axpasch  24569  exatleN  29593  ps-2b  29671  3atlem1  29672  3atlem2  29673  3atlem4  29675  3atlem5  29676  3atlem6  29677  2llnjaN  29755  2llnjN  29756  4atlem12b  29800  2lplnja  29808  2lplnj  29809  dalemrea  29817  dath2  29926  lneq2at  29967  osumcllem7N  30151  cdleme26ee  30549  cdlemg35  30902  cdlemg36  30903  cdlemj1  31010  cdlemk23-3  31091  cdlemk25-3  31093  cdlemk26b-3  31094  cdlemk27-3  31096  cdlemk28-3  31097  cdleml3N  31167
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator