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

Theorem simp122 1138
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp122  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ps )

Proof of Theorem simp122
StepHypRef Expression
1 simp22 1039 . 2  |-  ( ( th  /\  ( ph  /\ 
ps  /\  ch )  /\  ta )  ->  ps )
213ad2ant1 1026 1  |-  ( ( ( th  /\  ( ph  /\  ps  /\  ch )  /\  ta )  /\  et  /\  ze )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  ax5seglem3  24947  axpasch  24957  exatleN  32887  ps-2b  32965  3atlem1  32966  3atlem2  32967  3atlem4  32969  3atlem5  32970  3atlem6  32971  2llnjaN  33049  4atlem12b  33094  2lplnja  33102  dalemqea  33110  dath2  33220  lneq2at  33261  llnexchb2  33352  dalawlem1  33354  lhpexle3lem  33494  cdleme26ee  33845  cdlemg34  34197  cdlemg35  34198  cdlemg36  34199  cdlemj1  34306  cdlemj2  34307  cdlemk23-3  34387  cdlemk25-3  34389  cdlemk26b-3  34390  cdlemk26-3  34391  cdleml3N  34463
  Copyright terms: Public domain W3C validator