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

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

Proof of Theorem simpl13
StepHypRef Expression
1 simp13 1020 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ch )
21adantr 465 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ch )
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:  pythagtriplem4  13997  brbtwn2  23296  ax5seg  23329  br8  27703  btwndiff  28195  ifscgr  28212  seglecgr12im  28278  mply1topmatcl  31255  atlatle  33274  cvlcvr1  33293  atbtwn  33399  3dimlem3  33414  3dimlem3OLDN  33415  4atlem3  33549  4atlem11  33562  4atlem12  33565  2lplnj  33573  paddasslem4  33776  paddasslem10  33782  pmodlem1  33799  llnexchb2lem  33821  pclfinclN  33903  arglem1N  34143  cdlemd4  34154  cdlemd  34160  cdleme16  34238  cdleme20  34277  cdleme21k  34291  cdleme22cN  34295  cdleme27N  34322  cdleme28c  34325  cdleme29ex  34327  cdleme32fva  34390  cdleme40n  34421  cdlemg15a  34608  cdlemg15  34609  cdlemg16ALTN  34611  cdlemg16z  34612  cdlemg20  34638  cdlemg22  34640  cdlemg29  34658  cdlemg38  34668  cdlemk56  34924  dihord2pre  35179
  Copyright terms: Public domain W3C validator