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

Theorem simpl13 1072
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 1027 . 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 972
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 974
This theorem is referenced by:  pythagtriplem4  14217  mply1topmatcl  19176  brbtwn2  24077  ax5seg  24110  br8  29157  btwndiff  29649  ifscgr  29666  seglecgr12im  29732  fourierdlem77  31855  atlatle  34768  cvlcvr1  34787  atbtwn  34893  3dimlem3  34908  3dimlem3OLDN  34909  4atlem3  35043  4atlem11  35056  4atlem12  35059  2lplnj  35067  paddasslem4  35270  paddasslem10  35276  pmodlem1  35293  llnexchb2lem  35315  pclfinclN  35397  arglem1N  35638  cdlemd4  35649  cdlemd  35655  cdleme16  35733  cdleme20  35773  cdleme21k  35787  cdleme22cN  35791  cdleme27N  35818  cdleme28c  35821  cdleme29ex  35823  cdleme32fva  35886  cdleme40n  35917  cdlemg15a  36104  cdlemg15  36105  cdlemg16ALTN  36107  cdlemg16z  36108  cdlemg20  36134  cdlemg22  36136  cdlemg29  36154  cdlemg38  36164  cdlemk56  36420  dihord2pre  36675
  Copyright terms: Public domain W3C validator