MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp121 Structured version   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  25862  axpasch  25872  exatleN  30128  ps-2b  30206  3atlem1  30207  3atlem2  30208  3atlem4  30210  3atlem5  30211  3atlem6  30212  2llnjaN  30290  4atlem12b  30335  2lplnja  30343  dalempea  30350  dath2  30461  lneq2at  30502  llnexchb2  30593  dalawlem1  30595  osumcllem7N  30686  lhpexle3lem  30735  cdleme26ee  31084  cdlemg34  31436  cdlemg36  31438  cdlemj1  31545  cdlemj2  31546  cdlemk23-3  31626  cdlemk25-3  31628  cdlemk26b-3  31629  cdlemk26-3  31630  cdlemk27-3  31631  cdleml3N  31702
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