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  845  reupick3  3421  difprsnss  3731  trin2  5021  imadiflem  5296  fnun  5323  fco  5382  f1co  5434  foco  5449  f1oun  5482  f1oco  5485  eqfunfv  5619  ftpg  5701  issmo  6289  tfrlem5  6315  ener  6779  domtr  6785  unen  6816  xpdom2  6831  mapen  6846  pm54.43  7189  axpre-lttrn  7883  axpre-mulgt0  7886  zmulcl  9306  qaddcl  9635  qmulcl  9637  rpaddcl  9677  rpmulcl  9678  rpdivcl  9679  xrltnsym  9793  xrlttri3  9797  ge0addcl  9981  ge0mulcl  9982  ge0xaddcl  9983  expclzaplem  10544  expge0  10556  expge1  10557  hashfacen  10816  qredeu  12097  nn0gcdsq  12200  mul4sq  12392  cnovex  13699  iscn2  13703  txuni  13766  txcn  13778  lgsne0  14442  mul2sq  14466