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

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

Proof of Theorem simp121
StepHypRef Expression
1 simp21 990 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ph )
213ad2ant1 978 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  ax5seglem3  25577  axpasch  25587  exatleN  29569  ps-2b  29647  3atlem1  29648  3atlem2  29649  3atlem4  29651  3atlem5  29652  3atlem6  29653  2llnjaN  29731  4atlem12b  29776  2lplnja  29784  dalempea  29791  dath2  29902  lneq2at  29943  llnexchb2  30034  dalawlem1  30036  osumcllem7N  30127  lhpexle3lem  30176  cdleme26ee  30525  cdlemg34  30877  cdlemg36  30879  cdlemj1  30986  cdlemj2  30987  cdlemk23-3  31067  cdlemk25-3  31069  cdlemk26b-3  31070  cdlemk26-3  31071  cdlemk27-3  31072  cdleml3N  31143
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