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

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

Proof of Theorem simp132
StepHypRef Expression
1 simp32 1025 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ps )
213ad2ant1 1009 1  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  et  /\  ze )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 967
This theorem is referenced by:  ax5seglem3  23324  3atlem1  33446  3atlem2  33447  3atlem5  33450  2llnjaN  33529  4atlem11b  33571  4atlem12b  33574  lplncvrlvol2  33578  dalemtea  33593  dath2  33700  cdlemblem  33756  dalawlem1  33834  lhpexle3lem  33974  4atexlemex6  34037  cdleme22f2  34310  cdleme22g  34311  cdlemg7aN  34588  cdlemg34  34675  cdlemj1  34784  cdlemk23-3  34865  cdlemk25-3  34867  cdlemk26b-3  34868
  Copyright terms: Public domain W3C validator