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

Theorem simp21r 1112
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simp21r  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ps )

Proof of Theorem simp21r
StepHypRef Expression
1 simp1r 1019 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ps )
213ad2ant2 1016 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  modexp  12286  segconeu  29892  4atlem10  35746  lplncvrlvol2  35755  4atex  36216  4atex2-0cOLDN  36220  cdleme0moN  36366  cdleme16e  36423  cdleme17d1  36430  cdleme18d  36436  cdleme19d  36448  cdleme20f  36456  cdleme20g  36457  cdleme21ct  36471  cdleme22aa  36481  cdleme22cN  36484  cdleme22d  36485  cdleme22e  36486  cdleme22eALTN  36487  cdleme26e  36501  cdleme32e  36587  cdleme32f  36588  cdlemg4  36759  cdlemg18d  36823  cdlemg18  36824  cdlemg19a  36825  cdlemg19  36826  cdlemg21  36828  cdlemg33b0  36843  cdlemk5  36978  cdlemk6  36979  cdlemk7  36990  cdlemk11  36991  cdlemk12  36992  cdlemk21N  37015  cdlemk20  37016  cdlemk28-3  37050  cdlemk34  37052  cdlemkfid3N  37067  cdlemk55u1  37107
  Copyright terms: Public domain W3C validator