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  416  stdcndc  840  reupick3  3412  difprsnss  3718  trin2  5002  imadiflem  5277  fnun  5304  fco  5363  f1co  5415  foco  5430  f1oun  5462  f1oco  5465  eqfunfv  5598  ftpg  5680  issmo  6267  tfrlem5  6293  ener  6757  domtr  6763  unen  6794  xpdom2  6809  mapen  6824  pm54.43  7167  axpre-lttrn  7846  axpre-mulgt0  7849  zmulcl  9265  qaddcl  9594  qmulcl  9596  rpaddcl  9634  rpmulcl  9635  rpdivcl  9636  xrltnsym  9750  xrlttri3  9754  ge0addcl  9938  ge0mulcl  9939  ge0xaddcl  9940  expclzaplem  10500  expge0  10512  expge1  10513  hashfacen  10771  qredeu  12051  nn0gcdsq  12154  mul4sq  12346  cnovex  12990  iscn2  12994  txuni  13057  txcn  13069  lgsne0  13733  mul2sq  13746