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

Theorem simp122 1090
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 991 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ps )
213ad2ant1 978 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  ax5seglem3  25774  axpasch  25784  exatleN  29886  ps-2b  29964  3atlem1  29965  3atlem2  29966  3atlem4  29968  3atlem5  29969  3atlem6  29970  2llnjaN  30048  4atlem12b  30093  2lplnja  30101  dalemqea  30109  dath2  30219  lneq2at  30260  llnexchb2  30351  dalawlem1  30353  lhpexle3lem  30493  cdleme26ee  30842  cdlemg34  31194  cdlemg35  31195  cdlemg36  31196  cdlemj1  31303  cdlemj2  31304  cdlemk23-3  31384  cdlemk25-3  31386  cdlemk26b-3  31387  cdlemk26-3  31388  cdleml3N  31460
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator