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  5179  fundif  5425  imadiflem  5460  fnun  5489  fco  5552  f1co  5610  foco  5626  f1oun  5659  f1oco  5662  eqfunfv  5811  ftpg  5899  issmo  6559  tfrlem5  6585  ener  7066  domtr  7072  unen  7105  xpdom2  7129  mapen  7146  pm54.43  7536  axpre-lttrn  8251  axpre-mulgt0  8254  zmulcl  9698  qaddcl  10035  qmulcl  10037  rpaddcl  10078  rpmulcl  10079  rpdivcl  10080  xrltnsym  10195  xrlttri3  10199  ge0addcl  10383  ge0mulcl  10384  ge0xaddcl  10385  expclzaplem  11000  expge0  11012  expge1  11013  hashfacen  11284  qredeu  12875  nn0gcdsq  12978  mul4sq  13173  ballotfilem2  13228  cnovex  15297  iscn2  15301  txuni  15364  txcn  15376  lgsne0  16157  mul2sq  16235