Theorem syl2anb 465

Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)

Hypotheses

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

Assertion

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

Proof of Theorem syl2anb

Step	Hyp	Ref	Expression
1		syl2anb.2	. 2 |- (ta <-> ch)
2		syl2anb.1	. . 3 |- (ph <-> ps)
3		syl2anb.3	. . 3 |- ((ps /\ ch) -> th)
4	2, 3	sylanb 458	. 2 |- ((ph /\ ch) -> th)
5	1, 4	sylan2b 461	1 |- ((ph /\ ta) -> th)

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  sylancb  646  2eu6  2289  reupick3  3541  difprsnss  3847  ncfinraise  4482  ncfinlower  4484  sfinltfin  4536  fnun  5190  f1oun  5305  eqfunfv  5398  swapf1o  5512  fnfullfunlem2  5858  fvfullfunlem3  5864  xpassen  6058  enprmaplem3  6079  ncaddccl  6145  peano4nc  6151  cenc  6182