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

Theorem simp12r 1119
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 1032 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
213ad2ant1 1026 1  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ 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:  ackbij1lem16  8663  lsmcv  18299  nllyrest  20432  axcontlem4  24843  eqlkr  32374  athgt  32730  llncvrlpln2  32831  4atlem11b  32882  2lnat  33058  cdlemblem  33067  pclfinN  33174  lhp2at0nle  33309  4atexlemex6  33348  cdlemd2  33474  cdlemd8  33480  cdleme15a  33549  cdleme16b  33554  cdleme16c  33555  cdleme16d  33556  cdleme20h  33592  cdleme21c  33603  cdleme21ct  33605  cdleme22cN  33618  cdleme23b  33626  cdleme26fALTN  33638  cdleme26f  33639  cdleme26f2ALTN  33640  cdleme26f2  33641  cdleme32le  33723  cdleme35f  33730  cdlemf1  33837  trlord  33845  cdlemg7aN  33901  cdlemg33c0  33978  trlcone  34004  cdlemg44  34009  cdlemg48  34013  cdlemky  34202  cdlemk11ta  34205  cdleml4N  34255  dihmeetlem3N  34582  dihmeetlem13N  34596  mapdpglem32  34982  baerlem3lem2  34987  baerlem5alem2  34988  baerlem5blem2  34989  mzpcong  35528
  Copyright terms: Public domain W3C validator