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

Theorem simp121 1138
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 1039 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ph )
213ad2ant1 1027 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 983
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 189  df-an 373  df-3an 985
This theorem is referenced by:  ax5seglem3  24953  axpasch  24963  exatleN  32932  ps-2b  33010  3atlem1  33011  3atlem2  33012  3atlem4  33014  3atlem5  33015  3atlem6  33016  2llnjaN  33094  4atlem12b  33139  2lplnja  33147  dalempea  33154  dath2  33265  lneq2at  33306  llnexchb2  33397  dalawlem1  33399  osumcllem7N  33490  lhpexle3lem  33539  cdleme26ee  33890  cdlemg34  34242  cdlemg36  34244  cdlemj1  34351  cdlemj2  34352  cdlemk23-3  34432  cdlemk25-3  34434  cdlemk26b-3  34435  cdlemk26-3  34436  cdlemk27-3  34437  cdleml3N  34508
  Copyright terms: Public domain W3C validator