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  422  stdcndc  857  reupick3  3518  difprsnss  3848  trin2  5174  fundif  5420  imadiflem  5455  fnun  5484  fco  5547  f1co  5605  foco  5621  f1oun  5654  f1oco  5657  eqfunfv  5802  ftpg  5890  issmo  6549  tfrlem5  6575  ener  7056  domtr  7062  unen  7095  xpdom2  7119  mapen  7136  pm54.43  7526  axpre-lttrn  8241  axpre-mulgt0  8244  zmulcl  9677  qaddcl  10014  qmulcl  10016  rpaddcl  10057  rpmulcl  10058  rpdivcl  10059  xrltnsym  10174  xrlttri3  10178  ge0addcl  10362  ge0mulcl  10363  ge0xaddcl  10364  expclzaplem  10978  expge0  10990  expge1  10991  hashfacen  11262  qredeu  12853  nn0gcdsq  12956  mul4sq  13151  ballotfilem2  13206  cnovex  15220  iscn2  15224  txuni  15287  txcn  15299  lgsne0  16071  mul2sq  16149