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 7186  cvgratlem1ALT 7218  cvgratlem1 7221  ivthlem7 7258  ivthlem7OLD 7267  shsvst 9275  shintcl 9281  cvntrt 10210  cdj3 10359  ghomgsg 10386  hmphtr 10512  infi 10542  cmpmon 10692

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