Theorem 3simp2d 794

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 788	. 2 |- ((ps /\ ch /\ th) -> ch)
3	1, 2	syl 10	1 |- (ph -> ch)

Syntax hints:   -> wi 3   /\ w3a 774

This theorem is referenced by:  climaddlem3 7060  climmullem8 7071  isumcmpi 7158  abspef01tlub 7344  efcnlem2 7368  sin01bndlem2 7418  cos01bndlem2 7420  grpass 7997  subgres 8069  subgid 8072  subgabl 8075  vcsm 8120  nvf 8238  pilem3 8611  eigvect 9825  ghomgrplem 10323  ghomfo 10325  ghomgsg 10329  hmeocnb 10443  fillsb 10471  coda 10542  dehm 10600  iddvvidd 10632  idcvvidc 10633

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 776

Copyright terms: Public domain