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

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

Proof of Theorem simp21l
StepHypRef Expression
1 simp1l 1018 . 2  |-  ( ( ( ph  /\  ps )  /\  ch  /\  th )  ->  ph )
213ad2ant2 1016 1  |-  ( ( ta  /\  ( (
ph  /\  ps )  /\  ch  /\  th )  /\  et )  ->  ph )
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  12226  segconeu  29854  4atlem10  35782  lplncvrlvol2  35791  4atex  36252  4atex2-0cOLDN  36256  cdlemd2  36376  cdlemd3  36377  cdlemd4  36378  cdleme0e  36394  cdleme0moN  36402  cdleme3g  36411  cdleme3h  36412  cdleme3  36414  cdleme9  36430  cdleme11c  36438  cdleme11dN  36439  cdleme11e  36440  cdleme11fN  36441  cdleme11h  36443  cdleme11j  36444  cdleme11k  36445  cdleme11  36447  cdleme12  36448  cdleme13  36449  cdleme14  36450  cdleme15a  36451  cdleme15b  36452  cdleme15c  36453  cdleme15d  36454  cdleme15  36455  cdleme16b  36456  cdleme16c  36457  cdleme16d  36458  cdleme16e  36459  cdleme16f  36460  cdleme17d1  36466  cdleme18a  36468  cdleme18b  36469  cdleme18c  36470  cdleme18d  36472  cdleme19b  36482  cdleme19d  36484  cdleme19e  36485  cdleme20c  36489  cdleme20d  36490  cdleme20e  36491  cdleme20f  36492  cdleme20g  36493  cdleme20h  36494  cdleme20j  36496  cdleme20l2  36499  cdleme20l  36500  cdleme20m  36501  cdleme20  36502  cdleme21ct  36507  cdleme21e  36509  cdleme21i  36513  cdleme22aa  36517  cdleme22cN  36520  cdleme22d  36521  cdleme22e  36522  cdleme22eALTN  36523  cdleme22f  36524  cdleme26e  36537  cdleme27a  36545  cdleme32e  36623  cdlemg2fv2  36778  cdlemg4a  36786  cdlemg4d  36791  cdlemg4  36795  cdlemg6c  36798  cdlemg8b  36806  cdlemg8c  36807  cdlemg9a  36810  cdlemg9  36812  cdlemg12a  36821  cdlemg12c  36823  cdlemg17dALTN  36842  cdlemg17h  36846  cdlemg18b  36857  cdlemg18c  36858  cdlemg18d  36859  cdlemg18  36860  cdlemg19a  36861  cdlemg21  36864  cdlemg28a  36871  cdlemg31b0a  36873  cdlemg31d  36878  cdlemg33b0  36879  cdlemg33a  36884  cdlemh  36995  cdlemk5  37014  cdlemk6  37015  cdlemk7  37026  cdlemk11  37027  cdlemk12  37028  cdlemk21N  37051  cdlemk20  37052  cdlemk28-3  37086  cdlemk34  37088  cdlemkfid3N  37103  cdlemk35s-id  37116  cdlemk39s-id  37118  cdlemk55u1  37143  cdlemn2  37374  cdlemn10  37385  dihjustlem  37395
  Copyright terms: Public domain W3C validator