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

Theorem simpl13 1073
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 1028 . 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 973
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 975
This theorem is referenced by:  pythagtriplem4  14198  mply1topmatcl  19073  brbtwn2  23884  ax5seg  23917  br8  28762  btwndiff  29254  ifscgr  29271  seglecgr12im  29337  fourierdlem77  31484  atlatle  34117  cvlcvr1  34136  atbtwn  34242  3dimlem3  34257  3dimlem3OLDN  34258  4atlem3  34392  4atlem11  34405  4atlem12  34408  2lplnj  34416  paddasslem4  34619  paddasslem10  34625  pmodlem1  34642  llnexchb2lem  34664  pclfinclN  34746  arglem1N  34986  cdlemd4  34997  cdlemd  35003  cdleme16  35081  cdleme20  35120  cdleme21k  35134  cdleme22cN  35138  cdleme27N  35165  cdleme28c  35168  cdleme29ex  35170  cdleme32fva  35233  cdleme40n  35264  cdlemg15a  35451  cdlemg15  35452  cdlemg16ALTN  35454  cdlemg16z  35455  cdlemg20  35481  cdlemg22  35483  cdlemg29  35501  cdlemg38  35511  cdlemk56  35767  dihord2pre  36022
  Copyright terms: Public domain W3C validator