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  846  reupick3  3445  difprsnss  3757  trin2  5058  imadiflem  5334  fnun  5361  fco  5420  f1co  5472  foco  5488  f1oun  5521  f1oco  5524  eqfunfv  5661  ftpg  5743  issmo  6343  tfrlem5  6369  ener  6835  domtr  6841  unen  6872  xpdom2  6887  mapen  6904  pm54.43  7252  axpre-lttrn  7946  axpre-mulgt0  7949  zmulcl  9373  qaddcl  9703  qmulcl  9705  rpaddcl  9746  rpmulcl  9747  rpdivcl  9748  xrltnsym  9862  xrlttri3  9866  ge0addcl  10050  ge0mulcl  10051  ge0xaddcl  10052  expclzaplem  10637  expge0  10649  expge1  10650  hashfacen  10910  qredeu  12238  nn0gcdsq  12341  mul4sq  12535  cnovex  14375  iscn2  14379  txuni  14442  txcn  14454  lgsne0  15195  mul2sq  15273