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

Theorem simp122 1129
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 1030 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ps )
213ad2ant1 1017 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
This theorem is referenced by:  ax5seglem3  24057  axpasch  24067  exatleN  34601  ps-2b  34679  3atlem1  34680  3atlem2  34681  3atlem4  34683  3atlem5  34684  3atlem6  34685  2llnjaN  34763  4atlem12b  34808  2lplnja  34816  dalemqea  34824  dath2  34934  lneq2at  34975  llnexchb2  35066  dalawlem1  35068  lhpexle3lem  35208  cdleme26ee  35557  cdlemg34  35909  cdlemg35  35910  cdlemg36  35911  cdlemj1  36018  cdlemj2  36019  cdlemk23-3  36099  cdlemk25-3  36101  cdlemk26b-3  36102  cdlemk26-3  36103  cdleml3N  36175
  Copyright terms: Public domain W3C validator