Theorem 3simp2d 793

Description: Deduce a conjunct from a triple conjunction.

Hypothesis

Ref	Expression
3simp1d.1	|- (ph -> (ps /\ ch /\ th))

Assertion

Ref	Expression
3simp2d	|- (ph -> ch)

Proof of Theorem 3simp2d

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 |- (ph -> (ps /\ ch /\ th))
2		3simp2 787	. 2 |- ((ps /\ ch /\ th) -> ch)
3	1, 2	syl 10	1 |- (ph -> ch)

Syntax hints:   -> wi 3   /\ w3a 773

This theorem is referenced by:  climaddlem3 7052  climmullem8 7063  isumcmpi 7150  abspef01tlub 7336  efcnlem2 7360  sin01bndlem2 7410  cos01bndlem2 7412  grpass 7981  subgres 8054  subgid 8057  subgabl 8060  vcsm 8105  nvf 8226  pilem3 8592  eigvect 9802  ghomgrplem 10294  ghomfo 10296  ghomgsg 10300  hmeocnb 10407  fillsb 10435  coda 10506  dehm 10564  iddvvidd 10596  idcvvidc 10597

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 775

Copyright terms: Public domain