Theorem sylan2d 458

Description: A syllogism deduction.

Hypotheses

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

Assertion

Ref	Expression
sylan2d	|- (ph -> ((ps /\ ta) -> th))

Proof of Theorem sylan2d

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  syl2and 459  sylan2i 465  unblem1 4540  unfi 4551  unfiOLD 4552  ltbtwnpq 5084  prodgt02t 5827  prodge02t 5829  infpnlem1 7506  opnin 7869  bcthlem17 8015  shsubcltOLD 9090  shintcl 9293

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