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

Theorem simp121 1123
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 1024 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ph )
213ad2ant1 1012 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 968
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 970
This theorem is referenced by:  ax5seglem3  23903  axpasch  23913  exatleN  34075  ps-2b  34153  3atlem1  34154  3atlem2  34155  3atlem4  34157  3atlem5  34158  3atlem6  34159  2llnjaN  34237  4atlem12b  34282  2lplnja  34290  dalempea  34297  dath2  34408  lneq2at  34449  llnexchb2  34540  dalawlem1  34542  osumcllem7N  34633  lhpexle3lem  34682  cdleme26ee  35031  cdlemg34  35383  cdlemg36  35385  cdlemj1  35492  cdlemj2  35493  cdlemk23-3  35573  cdlemk25-3  35575  cdlemk26b-3  35576  cdlemk26-3  35577  cdlemk27-3  35578  cdleml3N  35649
  Copyright terms: Public domain W3C validator