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

Theorem simpl13 1032
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 987 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ch )
21adantr 451 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  pythagtriplem4  12888  br8  24184  brbtwn2  24605  ax5seg  24638  btwndiff  24722  ifscgr  24739  seglecgr12im  24805  islimrs4  25685  atlatle  30132  cvlcvr1  30151  atbtwn  30257  3dimlem3  30272  3dimlem3OLDN  30273  4atlem3  30407  4atlem11  30420  4atlem12  30423  2lplnj  30431  paddasslem4  30634  paddasslem10  30640  pmodlem1  30657  llnexchb2lem  30679  pclfinclN  30761  arglem1N  31001  cdlemd4  31012  cdlemd  31018  cdleme16  31096  cdleme20  31135  cdleme21k  31149  cdleme22cN  31153  cdleme27N  31180  cdleme28c  31183  cdleme29ex  31185  cdleme32fva  31248  cdleme40n  31279  cdlemg15a  31466  cdlemg15  31467  cdlemg16ALTN  31469  cdlemg16z  31470  cdlemg20  31496  cdlemg22  31498  cdlemg29  31516  cdlemg38  31526  cdlemk56  31782  dihord2pre  32037
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator