Theorem 3simp3d 796

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

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  iccsupr 6398  climaddlem3 7116  climmullem8 7127  isumcmpi 7215  ivthlem5 7285  efcnlem2 7420  lmcvg 7932  grplidinv 8045  subgres 8117  nvz 8297  nvtri 8298  pilem2 8672  sineq0 8713  adjt 9857  ghomgrplem 10389  hmeocna 10519  filint 10562  fipfil2 10564  fipfil2OLD 10565  ida 10663  cehm 10721

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 777

Copyright terms: Public domain