Theorem syl2anb 291

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 284	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	sylan2b 287	1 |- ( ( ph /\ ta ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylancb  418  stdcndc  850  reupick3  3490  difprsnss  3807  trin2  5124  fundif  5369  imadiflem  5404  fnun  5433  fco  5495  f1co  5549  foco  5565  f1oun  5598  f1oco  5601  eqfunfv  5743  ftpg  5831  issmo  6447  tfrlem5  6473  ener  6946  domtr  6952  unen  6984  xpdom2  7008  mapen  7025  pm54.43  7384  axpre-lttrn  8092  axpre-mulgt0  8095  zmulcl  9521  qaddcl  9857  qmulcl  9859  rpaddcl  9900  rpmulcl  9901  rpdivcl  9902  xrltnsym  10016  xrlttri3  10020  ge0addcl  10204  ge0mulcl  10205  ge0xaddcl  10206  expclzaplem  10813  expge0  10825  expge1  10826  hashfacen  11087  qredeu  12656  nn0gcdsq  12759  mul4sq  12954  cnovex  14907  iscn2  14911  txuni  14974  txcn  14986  lgsne0  15754  mul2sq  15832