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

Theorem simpl13 1082
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 1037 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ch )
21adantr 466 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th 
/\  ta )  /\  et )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  pythagtriplem4  14757  mply1topmatcl  19816  brbtwn2  24922  ax5seg  24955  br8  30391  btwndiff  30787  ifscgr  30804  seglecgr12im  30870  atlatle  32805  cvlcvr1  32824  atbtwn  32930  3dimlem3  32945  3dimlem3OLDN  32946  4atlem3  33080  4atlem11  33093  4atlem12  33096  2lplnj  33104  paddasslem4  33307  paddasslem10  33313  pmodlem1  33330  llnexchb2lem  33352  pclfinclN  33434  arglem1N  33675  cdlemd4  33686  cdlemd  33692  cdleme16  33770  cdleme20  33810  cdleme21k  33824  cdleme22cN  33828  cdleme27N  33855  cdleme28c  33858  cdleme29ex  33860  cdleme32fva  33923  cdleme40n  33954  cdlemg15a  34141  cdlemg15  34142  cdlemg16ALTN  34144  cdlemg16z  34145  cdlemg20  34171  cdlemg22  34173  cdlemg29  34191  cdlemg38  34201  cdlemk56  34457  dihord2pre  34712  uzwo4  37254  fourierdlem77  37867
  Copyright terms: Public domain W3C validator