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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylancb  422  stdcndc  857  reupick3  3518  difprsnss  3853  trin2  5182  fundif  5428  imadiflem  5463  fnun  5492  fco  5555  f1co  5613  foco  5629  f1oun  5662  f1oco  5665  eqfunfv  5814  ftpg  5902  issmo  6564  tfrlem5  6590  ener  7072  domtr  7078  unen  7111  xpdom2  7135  mapen  7152  pm54.43  7542  axpre-lttrn  8257  axpre-mulgt0  8260  zmulcl  9707  qaddcl  10050  qmulcl  10052  rpaddcl  10094  rpmulcl  10095  rpdivcl  10096  xrltnsym  10211  xrlttri3  10215  ge0addcl  10399  ge0mulcl  10400  ge0xaddcl  10401  expclzaplem  11020  expge0  11032  expge1  11033  hashfacen  11305  qredeu  12899  nn0gcdsq  13004  mul4sq  13201  ballotfilem2  13285  cnovex  15439  iscn2  15443  txuni  15506  txcn  15518  efnnfsumcl  16256  efchtqdvds  16282  lgsne0  16379  mul2sq  16457