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

Theorem simp121 1126
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 1027 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ph )
213ad2ant1 1015 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  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  axpasch  24446  exatleN  35525  ps-2b  35603  3atlem1  35604  3atlem2  35605  3atlem4  35607  3atlem5  35608  3atlem6  35609  2llnjaN  35687  4atlem12b  35732  2lplnja  35740  dalempea  35747  dath2  35858  lneq2at  35899  llnexchb2  35990  dalawlem1  35992  osumcllem7N  36083  lhpexle3lem  36132  cdleme26ee  36483  cdlemg34  36835  cdlemg36  36837  cdlemj1  36944  cdlemj2  36945  cdlemk23-3  37025  cdlemk25-3  37027  cdlemk26b-3  37028  cdlemk26-3  37029  cdlemk27-3  37030  cdleml3N  37101
  Copyright terms: Public domain W3C validator