Theorem 3simp3d 794

Description: Deduce a conjunct from a triple conjunction.

Hypothesis

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

Assertion

Ref	Expression
3simp3d	|- (ph -> th)

Proof of Theorem 3simp3d

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

Syntax hints:   -> wi 3   /\ w3a 773

This theorem is referenced by:  iccsupr 6331  climaddlem3 7052  climmullem8 7063  isumcmpi 7150  ivthlem5 7220  ivthlem4OLD 7228  ivthlem5OLD 7229  efcnlem2 7360  lmcvg 7870  grplidinv 7979  subgres 8054  nvz 8236  nvtri 8237  pilem2 8591  adjt 9773  ghomgrplem 10294  hmeocna 10406  filint 10437  fipfil2 10439  ida 10507  cehm 10565

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