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  12872  br8  24113  brbtwn2  24533  ax5seg  24566  btwndiff  24650  ifscgr  24667  seglecgr12im  24733  islimrs4  25582  atlatle  29510  cvlcvr1  29529  atbtwn  29635  3dimlem3  29650  3dimlem3OLDN  29651  4atlem3  29785  4atlem11  29798  4atlem12  29801  2lplnj  29809  paddasslem4  30012  paddasslem10  30018  pmodlem1  30035  llnexchb2lem  30057  pclfinclN  30139  arglem1N  30379  cdlemd4  30390  cdlemd  30396  cdleme16  30474  cdleme20  30513  cdleme21k  30527  cdleme22cN  30531  cdleme27N  30558  cdleme28c  30561  cdleme29ex  30563  cdleme32fva  30626  cdleme40n  30657  cdlemg15a  30844  cdlemg15  30845  cdlemg16ALTN  30847  cdlemg16z  30848  cdlemg20  30874  cdlemg22  30876  cdlemg29  30894  cdlemg38  30904  cdlemk56  31160  dihord2pre  31415
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