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

Theorem simpl31 1069
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 1024 . 2  |-  ( ( th  /\  ta  /\  ( ph  /\  ps  /\  ch ) )  ->  ph )
21adantr 465 1  |-  ( ( ( th  /\  ta  /\  ( ph  /\  ps  /\ 
ch ) )  /\  et )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  ax5seglem3a  23311  ax5seg  23319  br8d  26076  br8  27700  cgrextend  28173  segconeq  28175  trisegint  28193  ifscgr  28209  cgrsub  28210  btwnxfr  28221  seglecgr12im  28275  segletr  28279  atbtwn  33396  3dim1  33417  2llnjaN  33516  4atlem10b  33555  4atlem11  33559  4atlem12  33562  2lplnj  33570  paddasslem4  33773  pmodlem1  33796  4atex2  34027  trlval3  34137  arglem1N  34140  cdleme0moN  34175  cdleme17b  34237  cdleme20  34274  cdleme21j  34286  cdleme28c  34322  cdleme35h2  34407  cdlemg6c  34570  cdlemg6  34573  cdlemg7N  34576  cdlemg8c  34579  cdlemg11a  34587  cdlemg11b  34592  cdlemg12e  34597  cdlemg16  34607  cdlemg16ALTN  34608  cdlemg16zz  34610  cdlemg20  34635  cdlemg22  34637  cdlemg37  34639  cdlemg31d  34650  cdlemg33b  34657  cdlemg33  34661  cdlemg39  34666  cdlemg42  34679  cdlemk25-3  34854  cdlemk33N  34859  cdlemk53b  34906
  Copyright terms: Public domain W3C validator