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  3506  difprsnss  3832  trin2  5154  fundif  5400  imadiflem  5435  fnun  5464  fco  5527  f1co  5585  foco  5601  f1oun  5634  f1oco  5637  eqfunfv  5780  ftpg  5868  issmo  6519  tfrlem5  6545  ener  7019  domtr  7025  unen  7058  xpdom2  7082  mapen  7099  pm54.43  7487  axpre-lttrn  8199  axpre-mulgt0  8202  zmulcl  9631  qaddcl  9967  qmulcl  9969  rpaddcl  10010  rpmulcl  10011  rpdivcl  10012  xrltnsym  10126  xrlttri3  10130  ge0addcl  10314  ge0mulcl  10315  ge0xaddcl  10316  expclzaplem  10925  expge0  10937  expge1  10938  hashfacen  11208  qredeu  12794  nn0gcdsq  12897  mul4sq  13092  ballotfilem2  13142  cnovex  15061  iscn2  15065  txuni  15128  txcn  15140  lgsne0  15911  mul2sq  15989