Theorem 3simp3d 808

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

Syntax hints:   -> wi 3   /\ w3a 787

This theorem is referenced by:  intfracq 6367  fldiv 6368  iccsupr 6424  climaddlem3 7206  climmullem8 7217  isumcmpii 7305  ivthlem5 7375  efcnlem2 7511  lmcvg 8017  grplidinv 8130  subgres 8201  nvz 8381  nvtri 8382  pilem2 8755  sineq0 8796  adj1 9940  ghomgrplem 10474  hmeocna 10613  filint 10656  fipfil2 10658  ida 10745  cehm 10803

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