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

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

Proof of Theorem simpl31
StepHypRef Expression
1 simp31 1030 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ph )
21adantr 463 1  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  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:  ax5seglem3a  24438  ax5seg  24446  br8d  27681  br8  29429  cgrextend  29889  segconeq  29891  trisegint  29909  ifscgr  29925  cgrsub  29926  btwnxfr  29937  seglecgr12im  29991  segletr  29995  atbtwn  35586  3dim1  35607  2llnjaN  35706  4atlem10b  35745  4atlem11  35749  4atlem12  35752  2lplnj  35760  paddasslem4  35963  pmodlem1  35986  4atex2  36217  trlval3  36328  arglem1N  36331  cdleme0moN  36366  cdleme17b  36428  cdleme20  36466  cdleme21j  36478  cdleme28c  36514  cdleme35h2  36599  cdlemg6c  36762  cdlemg6  36765  cdlemg7N  36768  cdlemg8c  36771  cdlemg11a  36779  cdlemg11b  36784  cdlemg12e  36789  cdlemg16  36799  cdlemg16ALTN  36800  cdlemg16zz  36802  cdlemg20  36827  cdlemg22  36829  cdlemg37  36831  cdlemg31d  36842  cdlemg33b  36849  cdlemg33  36853  cdlemg39  36858  cdlemg42  36871  cdlemk25-3  37046  cdlemk33N  37051  cdlemk53b  37098
  Copyright terms: Public domain W3C validator