Theorem sylan2d 460

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 439	. . 3 |- (ph -> ((ch /\ ps) -> th))
3		sylan2d.2	. . 3 |- (ph -> (ta -> ch))
4	2, 3	syland 459	. 2 |- (ph -> ((ta /\ ps) -> th))
5	4	ancomsd 439	1 |- (ph -> ((ps /\ ta) -> th))

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  syl2and 461  sylan2i 467  unblem1 4551  unfi 4563  unfiOLD 4564  ltbtwnpq 5096  prodgt02t 5829  prodge02t 5831  infpnlem1 7507  opnin 7866  bcthlem17 8012  shsubcltOLD 9085  shintcl 9288

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