Theorem syl2anb 289

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylancb  414  stdcndc  830  reupick3  3361  difprsnss  3658  trin2  4930  imadiflem  5202  fnun  5229  fco  5288  f1co  5340  foco  5355  f1oun  5387  f1oco  5390  eqfunfv  5523  ftpg  5604  issmo  6185  tfrlem5  6211  ener  6673  domtr  6679  unen  6710  xpdom2  6725  mapen  6740  pm54.43  7046  axpre-lttrn  7692  axpre-mulgt0  7695  zmulcl  9107  qaddcl  9427  qmulcl  9429  rpaddcl  9465  rpmulcl  9466  rpdivcl  9467  xrltnsym  9579  xrlttri3  9583  ge0addcl  9764  ge0mulcl  9765  ge0xaddcl  9766  expclzaplem  10317  expge0  10329  expge1  10330  hashfacen  10579  qredeu  11778  nn0gcdsq  11878  cnovex  12365  iscn2  12369  txuni  12432  txcn  12444