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  847  reupick3  3462  difprsnss  3777  trin2  5083  fundif  5327  imadiflem  5362  fnun  5391  fco  5451  f1co  5505  foco  5521  f1oun  5554  f1oco  5557  eqfunfv  5695  ftpg  5781  issmo  6387  tfrlem5  6413  ener  6884  domtr  6890  unen  6922  xpdom2  6941  mapen  6958  pm54.43  7313  axpre-lttrn  8017  axpre-mulgt0  8020  zmulcl  9446  qaddcl  9776  qmulcl  9778  rpaddcl  9819  rpmulcl  9820  rpdivcl  9821  xrltnsym  9935  xrlttri3  9939  ge0addcl  10123  ge0mulcl  10124  ge0xaddcl  10125  expclzaplem  10730  expge0  10742  expge1  10743  hashfacen  11003  qredeu  12494  nn0gcdsq  12597  mul4sq  12792  cnovex  14743  iscn2  14747  txuni  14810  txcn  14822  lgsne0  15590  mul2sq  15668