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

Theorem simp122 1088
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp122  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ps )

Proof of Theorem simp122
StepHypRef Expression
1 simp22 989 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ps )
213ad2ant1 976 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ps )
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  4atlem12b  29800  2lplnja  29808  dalemqea  29816  dath2  29926  lneq2at  29967  llnexchb2  30058  dalawlem1  30060  lhpexle3lem  30200  cdleme26ee  30549  cdlemg34  30901  cdlemg35  30902  cdlemg36  30903  cdlemj1  31010  cdlemj2  31011  cdlemk23-3  31091  cdlemk25-3  31093  cdlemk26b-3  31094  cdlemk26-3  31095  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