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  853  reupick3  3494  difprsnss  3816  trin2  5135  fundif  5381  imadiflem  5416  fnun  5445  fco  5507  f1co  5563  foco  5579  f1oun  5612  f1oco  5615  eqfunfv  5758  ftpg  5846  issmo  6497  tfrlem5  6523  ener  6996  domtr  7002  unen  7034  xpdom2  7058  mapen  7075  pm54.43  7438  axpre-lttrn  8147  axpre-mulgt0  8150  zmulcl  9577  qaddcl  9913  qmulcl  9915  rpaddcl  9956  rpmulcl  9957  rpdivcl  9958  xrltnsym  10072  xrlttri3  10076  ge0addcl  10260  ge0mulcl  10261  ge0xaddcl  10262  expclzaplem  10871  expge0  10883  expge1  10884  hashfacen  11146  qredeu  12732  nn0gcdsq  12835  mul4sq  13030  cnovex  14990  iscn2  14994  txuni  15057  txcn  15069  lgsne0  15840  mul2sq  15918