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

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

Proof of Theorem simp12r
StepHypRef Expression
1 simp2r 984 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
213ad2ant1 978 1  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  ackbij1lem16  8048  lsmcv  16140  nllyrest  17470  axcontlem4  25620  mzpcong  26728  eqlkr  29214  athgt  29570  llncvrlpln2  29671  4atlem11b  29722  2lnat  29898  cdlemblem  29907  pclfinN  30014  lhp2at0nle  30149  4atexlemex6  30188  cdlemd2  30313  cdlemd8  30319  cdleme15a  30388  cdleme16b  30393  cdleme16c  30394  cdleme16d  30395  cdleme20h  30430  cdleme21c  30441  cdleme21ct  30443  cdleme22cN  30456  cdleme23b  30464  cdleme26fALTN  30476  cdleme26f  30477  cdleme26f2ALTN  30478  cdleme26f2  30479  cdleme32le  30561  cdleme35f  30568  cdlemf1  30675  trlord  30683  cdlemg7aN  30739  cdlemg33c0  30816  trlcone  30842  cdlemg44  30847  cdlemg48  30851  cdlemky  31040  cdlemk11ta  31043  cdleml4N  31093  dihmeetlem3N  31420  dihmeetlem13N  31434  mapdpglem32  31820  baerlem3lem2  31825  baerlem5alem2  31826  baerlem5blem2  31827
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