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  7877  lsmcv  15910  nllyrest  17228  axcontlem4  24667  prdnei  25676  mzpcong  27162  eqlkr  29911  athgt  30267  llncvrlpln2  30368  4atlem11b  30419  2lnat  30595  cdlemblem  30604  pclfinN  30711  lhp2at0nle  30846  4atexlemex6  30885  cdlemd2  31010  cdlemd8  31016  cdleme15a  31085  cdleme16b  31090  cdleme16c  31091  cdleme16d  31092  cdleme20h  31127  cdleme21c  31138  cdleme21ct  31140  cdleme22cN  31153  cdleme23b  31161  cdleme26fALTN  31173  cdleme26f  31174  cdleme26f2ALTN  31175  cdleme26f2  31176  cdleme32le  31258  cdleme35f  31265  cdlemf1  31372  trlord  31380  cdlemg7aN  31436  cdlemg33c0  31513  trlcone  31539  cdlemg44  31544  cdlemg48  31548  cdlemky  31737  cdlemk11ta  31740  cdleml4N  31790  dihmeetlem3N  32117  dihmeetlem13N  32131  mapdpglem32  32517  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524
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