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  9702  qaddcl  10044  qmulcl  10046  rpaddcl  10088  rpmulcl  10089  rpdivcl  10090  xrltnsym  10205  xrlttri3  10209  ge0addcl  10393  ge0mulcl  10394  ge0xaddcl  10395  expclzaplem  11013  expge0  11025  expge1  11026  hashfacen  11298  qredeu  12891  nn0gcdsq  12996  mul4sq  13193  ballotfilem2  13277  cnovex  15346  iscn2  15350  txuni  15413  txcn  15425  lgsne0  16255  mul2sq  16333