MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simpl13 Structured version   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  13183  br8  25369  brbtwn2  25809  ax5seg  25842  btwndiff  25926  ifscgr  25943  seglecgr12im  26009  atlatle  30019  cvlcvr1  30038  atbtwn  30144  3dimlem3  30159  3dimlem3OLDN  30160  4atlem3  30294  4atlem11  30307  4atlem12  30310  2lplnj  30318  paddasslem4  30521  paddasslem10  30527  pmodlem1  30544  llnexchb2lem  30566  pclfinclN  30648  arglem1N  30888  cdlemd4  30899  cdlemd  30905  cdleme16  30983  cdleme20  31022  cdleme21k  31036  cdleme22cN  31040  cdleme27N  31067  cdleme28c  31070  cdleme29ex  31072  cdleme32fva  31135  cdleme40n  31166  cdlemg15a  31353  cdlemg15  31354  cdlemg16ALTN  31356  cdlemg16z  31357  cdlemg20  31383  cdlemg22  31385  cdlemg29  31403  cdlemg38  31413  cdlemk56  31669  dihord2pre  31924
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