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  846  reupick3  3457  difprsnss  3770  trin2  5071  imadiflem  5347  fnun  5376  fco  5435  f1co  5487  foco  5503  f1oun  5536  f1oco  5539  eqfunfv  5676  ftpg  5758  issmo  6364  tfrlem5  6390  ener  6856  domtr  6862  unen  6893  xpdom2  6908  mapen  6925  pm54.43  7280  axpre-lttrn  7979  axpre-mulgt0  7982  zmulcl  9408  qaddcl  9738  qmulcl  9740  rpaddcl  9781  rpmulcl  9782  rpdivcl  9783  xrltnsym  9897  xrlttri3  9901  ge0addcl  10085  ge0mulcl  10086  ge0xaddcl  10087  expclzaplem  10689  expge0  10701  expge1  10702  hashfacen  10962  qredeu  12338  nn0gcdsq  12441  mul4sq  12636  cnovex  14586  iscn2  14590  txuni  14653  txcn  14665  lgsne0  15433  mul2sq  15511