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

Theorem simpl13 1034
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 989 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ch )
21adantr 452 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  pythagtriplem4  13121  br8  25138  brbtwn2  25559  ax5seg  25592  btwndiff  25676  ifscgr  25693  seglecgr12im  25759  atlatle  29436  cvlcvr1  29455  atbtwn  29561  3dimlem3  29576  3dimlem3OLDN  29577  4atlem3  29711  4atlem11  29724  4atlem12  29727  2lplnj  29735  paddasslem4  29938  paddasslem10  29944  pmodlem1  29961  llnexchb2lem  29983  pclfinclN  30065  arglem1N  30305  cdlemd4  30316  cdlemd  30322  cdleme16  30400  cdleme20  30439  cdleme21k  30453  cdleme22cN  30457  cdleme27N  30484  cdleme28c  30487  cdleme29ex  30489  cdleme32fva  30552  cdleme40n  30583  cdlemg15a  30770  cdlemg15  30771  cdlemg16ALTN  30773  cdlemg16z  30774  cdlemg20  30800  cdlemg22  30802  cdlemg29  30820  cdlemg38  30830  cdlemk56  31086  dihord2pre  31341
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator