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  25584  axpasch  25594  exatleN  29518  ps-2b  29596  3atlem1  29597  3atlem2  29598  3atlem4  29600  3atlem5  29601  3atlem6  29602  2llnjaN  29680  4atlem12b  29725  2lplnja  29733  dalemqea  29741  dath2  29851  lneq2at  29892  llnexchb2  29983  dalawlem1  29985  lhpexle3lem  30125  cdleme26ee  30474  cdlemg34  30826  cdlemg35  30827  cdlemg36  30828  cdlemj1  30935  cdlemj2  30936  cdlemk23-3  31016  cdlemk25-3  31018  cdlemk26b-3  31019  cdlemk26-3  31020  cdleml3N  31092
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