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

Theorem simp132 1093
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 994 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ps )
213ad2ant1 978 1  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  et  /\  ze )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  ax5seglem3  25584  3atlem1  29597  3atlem2  29598  3atlem5  29601  2llnjaN  29680  4atlem11b  29722  4atlem12b  29725  lplncvrlvol2  29729  dalemtea  29744  dath2  29851  cdlemblem  29907  dalawlem1  29985  lhpexle3lem  30125  4atexlemex6  30188  cdleme22f2  30461  cdleme22g  30462  cdlemg7aN  30739  cdlemg34  30826  cdlemj1  30935  cdlemk23-3  31016  cdlemk25-3  31018  cdlemk26b-3  31019
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