Theorem syl2and 459

Description: A syllogism deduction.

Hypotheses

Ref	Expression
syl2and.1	|- (ph -> ((ps /\ ch) -> th))
syl2and.2	|- (ph -> (ta -> ps))
syl2and.3	|- (ph -> (et -> ch))

Assertion

Ref	Expression
syl2and	|- (ph -> ((ta /\ et) -> th))

Proof of Theorem syl2and

Step	Hyp	Ref	Expression
1		syl2and.1	. . 3 |- (ph -> ((ps /\ ch) -> th))
2		syl2and.3	. . 3 |- (ph -> (et -> ch))
3	1, 2	sylan2d 458	. 2 |- (ph -> ((ps /\ et) -> th))
4		syl2and.2	. 2 |- (ph -> (ta -> ps))
5	3, 4	syland 457	1 |- (ph -> ((ta /\ et) -> th))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  isumcmpi 7215  cvgratlem1ALT 7247  cvgratlem1 7250  ivthlem7 7287  shsvst 9287  shintcl 9293  cvntrt 10219  cdj3 10368  ghomgsg 10395  hmphtr 10531  infi 10578  infiOLD 10579  cmpmon 10743

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

Copyright terms: Public domain