Theorem syl2anb 289

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 282	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	sylan2b 285	1 |- ( ( ph /\ ta ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylancb  414  stdcndc  830  reupick3  3356  difprsnss  3653  trin2  4925  imadiflem  5197  fnun  5224  fco  5283  f1co  5335  foco  5350  f1oun  5380  f1oco  5383  eqfunfv  5516  ftpg  5597  issmo  6178  tfrlem5  6204  ener  6666  domtr  6672  unen  6703  xpdom2  6718  mapen  6733  pm54.43  7039  axpre-lttrn  7685  axpre-mulgt0  7688  zmulcl  9100  qaddcl  9420  qmulcl  9422  rpaddcl  9458  rpmulcl  9459  rpdivcl  9460  xrltnsym  9572  xrlttri3  9576  ge0addcl  9757  ge0mulcl  9758  ge0xaddcl  9759  expclzaplem  10310  expge0  10322  expge1  10323  hashfacen  10572  qredeu  11767  nn0gcdsq  11867  cnovex  12354  iscn2  12358  txuni  12421  txcn  12433