MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp122 Structured version   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  25862  axpasch  25872  exatleN  30128  ps-2b  30206  3atlem1  30207  3atlem2  30208  3atlem4  30210  3atlem5  30211  3atlem6  30212  2llnjaN  30290  4atlem12b  30335  2lplnja  30343  dalemqea  30351  dath2  30461  lneq2at  30502  llnexchb2  30593  dalawlem1  30595  lhpexle3lem  30735  cdleme26ee  31084  cdlemg34  31436  cdlemg35  31437  cdlemg36  31438  cdlemj1  31545  cdlemj2  31546  cdlemk23-3  31626  cdlemk25-3  31628  cdlemk26b-3  31629  cdlemk26-3  31630  cdleml3N  31702
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