Theorem 3simp2d 807

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

Syntax hints:   -> wi 3   /\ w3a 787

This theorem is referenced by:  fldiv 6368  climaddlem3 7206  climmullem8 7217  isumcmpii 7305  abspef01tlubi 7486  efcnlem2 7511  sin01bndlem2 7560  cos01bndlem2 7562  grpass 8132  subgres 8201  subgid 8204  subgabl 8207  vcsm 8252  nvf 8370  pilem3 8756  eigvec1 9969  ghomgrplem 10474  ghomfo 10476  ghomgsg 10480  hmeocnb 10614  fillsb 10654  coda 10744  dehm 10802  iddvvidd 10842  idcvvidc 10843

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 154  df-an 232  df-3an 789

Copyright terms: Public domain