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  3809  trin2  5126  fundif  5371  imadiflem  5406  fnun  5435  fco  5497  f1co  5551  foco  5567  f1oun  5600  f1oco  5603  eqfunfv  5745  ftpg  5833  issmo  6449  tfrlem5  6475  ener  6948  domtr  6954  unen  6986  xpdom2  7010  mapen  7027  pm54.43  7386  axpre-lttrn  8094  axpre-mulgt0  8097  zmulcl  9523  qaddcl  9859  qmulcl  9861  rpaddcl  9902  rpmulcl  9903  rpdivcl  9904  xrltnsym  10018  xrlttri3  10022  ge0addcl  10206  ge0mulcl  10207  ge0xaddcl  10208  expclzaplem  10815  expge0  10827  expge1  10828  hashfacen  11090  qredeu  12659  nn0gcdsq  12762  mul4sq  12957  cnovex  14910  iscn2  14914  txuni  14977  txcn  14989  lgsne0  15757  mul2sq  15835