MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp12r Structured version   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  8107  lsmcv  16205  nllyrest  17541  axcontlem4  25898  mzpcong  27018  eqlkr  29824  athgt  30180  llncvrlpln2  30281  4atlem11b  30332  2lnat  30508  cdlemblem  30517  pclfinN  30624  lhp2at0nle  30759  4atexlemex6  30798  cdlemd2  30923  cdlemd8  30929  cdleme15a  30998  cdleme16b  31003  cdleme16c  31004  cdleme16d  31005  cdleme20h  31040  cdleme21c  31051  cdleme21ct  31053  cdleme22cN  31066  cdleme23b  31074  cdleme26fALTN  31086  cdleme26f  31087  cdleme26f2ALTN  31088  cdleme26f2  31089  cdleme32le  31171  cdleme35f  31178  cdlemf1  31285  trlord  31293  cdlemg7aN  31349  cdlemg33c0  31426  trlcone  31452  cdlemg44  31457  cdlemg48  31461  cdlemky  31650  cdlemk11ta  31653  cdleml4N  31703  dihmeetlem3N  32030  dihmeetlem13N  32044  mapdpglem32  32430  baerlem3lem2  32435  baerlem5alem2  32436  baerlem5blem2  32437
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