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  3510  difprsnss  3837  trin2  5159  fundif  5405  imadiflem  5440  fnun  5469  fco  5532  f1co  5590  foco  5606  f1oun  5639  f1oco  5642  eqfunfv  5785  ftpg  5873  issmo  6532  tfrlem5  6558  ener  7032  domtr  7038  unen  7071  xpdom2  7095  mapen  7112  pm54.43  7500  axpre-lttrn  8215  axpre-mulgt0  8218  zmulcl  9648  qaddcl  9985  qmulcl  9987  rpaddcl  10028  rpmulcl  10029  rpdivcl  10030  xrltnsym  10145  xrlttri3  10149  ge0addcl  10333  ge0mulcl  10334  ge0xaddcl  10335  expclzaplem  10949  expge0  10961  expge1  10962  hashfacen  11233  qredeu  12819  nn0gcdsq  12922  mul4sq  13117  ballotfilem2  13172  cnovex  15187  iscn2  15191  txuni  15254  txcn  15266  lgsne0  16037  mul2sq  16115