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  30138  ps-2b  30216  3atlem1  30217  3atlem2  30218  3atlem4  30220  3atlem5  30221  3atlem6  30222  2llnjaN  30300  4atlem12b  30345  2lplnja  30353  dalempea  30360  dath2  30471  lneq2at  30512  llnexchb2  30603  dalawlem1  30605  osumcllem7N  30696  lhpexle3lem  30745  cdleme26ee  31094  cdlemg34  31446  cdlemg36  31448  cdlemj1  31555  cdlemj2  31556  cdlemk23-3  31636  cdlemk25-3  31638  cdlemk26b-3  31639  cdlemk26-3  31640  cdlemk27-3  31641  cdleml3N  31712
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