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

Theorem simp12r 1069
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 982 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
213ad2ant1 976 1  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  ackbij1lem16  7861  lsmcv  15894  nllyrest  17212  axcontlem4  24595  prdnei  25573  mzpcong  27059  eqlkr  29289  athgt  29645  llncvrlpln2  29746  4atlem11b  29797  2lnat  29973  cdlemblem  29982  pclfinN  30089  lhp2at0nle  30224  4atexlemex6  30263  cdlemd2  30388  cdlemd8  30394  cdleme15a  30463  cdleme16b  30468  cdleme16c  30469  cdleme16d  30470  cdleme20h  30505  cdleme21c  30516  cdleme21ct  30518  cdleme22cN  30531  cdleme23b  30539  cdleme26fALTN  30551  cdleme26f  30552  cdleme26f2ALTN  30553  cdleme26f2  30554  cdleme32le  30636  cdleme35f  30643  cdlemf1  30750  trlord  30758  cdlemg7aN  30814  cdlemg33c0  30891  trlcone  30917  cdlemg44  30922  cdlemg48  30926  cdlemky  31115  cdlemk11ta  31118  cdleml4N  31168  dihmeetlem3N  31495  dihmeetlem13N  31509  mapdpglem32  31895  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator