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

Theorem simp12r 1110
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 1023 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ps )
213ad2ant1 1017 1  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 973
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 975
This theorem is referenced by:  ackbij1lem16  8615  lsmcv  17587  nllyrest  19781  axcontlem4  23974  mzpcong  30542  eqlkr  33914  athgt  34270  llncvrlpln2  34371  4atlem11b  34422  2lnat  34598  cdlemblem  34607  pclfinN  34714  lhp2at0nle  34849  4atexlemex6  34888  cdlemd2  35013  cdlemd8  35019  cdleme15a  35088  cdleme16b  35093  cdleme16c  35094  cdleme16d  35095  cdleme20h  35130  cdleme21c  35141  cdleme21ct  35143  cdleme22cN  35156  cdleme23b  35164  cdleme26fALTN  35176  cdleme26f  35177  cdleme26f2ALTN  35178  cdleme26f2  35179  cdleme32le  35261  cdleme35f  35268  cdlemf1  35375  trlord  35383  cdlemg7aN  35439  cdlemg33c0  35516  trlcone  35542  cdlemg44  35547  cdlemg48  35551  cdlemky  35740  cdlemk11ta  35743  cdleml4N  35793  dihmeetlem3N  36120  dihmeetlem13N  36134  mapdpglem32  36520  baerlem3lem2  36525  baerlem5alem2  36526  baerlem5blem2  36527
  Copyright terms: Public domain W3C validator