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

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

Proof of Theorem simp131
StepHypRef Expression
1 simp31 1030 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ph )
213ad2ant1 1015 1  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  et  /\  ze )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  ax5seglem3  24436  exatleN  35525  3atlem1  35604  3atlem2  35605  3atlem5  35608  2llnjaN  35687  4atlem11b  35729  4atlem12b  35732  lplncvrlvol2  35736  dalemsea  35750  dath2  35858  cdlemblem  35914  dalawlem1  35992  lhpexle3lem  36132  4atexlemex6  36195  cdleme22f2  36470  cdleme22g  36471  cdlemg7aN  36748  cdlemg34  36835  cdlemj1  36944  cdlemk23-3  37025  cdlemk25-3  37027  cdlemk26b-3  37028  cdleml3N  37101
  Copyright terms: Public domain W3C validator