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

Theorem simp12r 1102
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 1015 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
213ad2ant1 1009 1  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  ackbij1lem16  8409  lsmcv  17227  nllyrest  19095  axcontlem4  23218  mzpcong  29320  eqlkr  32749  athgt  33105  llncvrlpln2  33206  4atlem11b  33257  2lnat  33433  cdlemblem  33442  pclfinN  33549  lhp2at0nle  33684  4atexlemex6  33723  cdlemd2  33848  cdlemd8  33854  cdleme15a  33923  cdleme16b  33928  cdleme16c  33929  cdleme16d  33930  cdleme20h  33965  cdleme21c  33976  cdleme21ct  33978  cdleme22cN  33991  cdleme23b  33999  cdleme26fALTN  34011  cdleme26f  34012  cdleme26f2ALTN  34013  cdleme26f2  34014  cdleme32le  34096  cdleme35f  34103  cdlemf1  34210  trlord  34218  cdlemg7aN  34274  cdlemg33c0  34351  trlcone  34377  cdlemg44  34382  cdlemg48  34386  cdlemky  34575  cdlemk11ta  34578  cdleml4N  34628  dihmeetlem3N  34955  dihmeetlem13N  34969  mapdpglem32  35355  baerlem3lem2  35360  baerlem5alem2  35361  baerlem5blem2  35362
  Copyright terms: Public domain W3C validator