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  7537  axpre-lttrn  8252  axpre-mulgt0  8255  zmulcl  9703  qaddcl  10045  qmulcl  10047  rpaddcl  10089  rpmulcl  10090  rpdivcl  10091  xrltnsym  10206  xrlttri3  10210  ge0addcl  10394  ge0mulcl  10395  ge0xaddcl  10396  expclzaplem  11015  expge0  11027  expge1  11028  hashfacen  11300  qredeu  12894  nn0gcdsq  12999  mul4sq  13196  ballotfilem2  13280  cnovex  15388  iscn2  15392  txuni  15455  txcn  15467  efnnfsumcl  16200  efchtqdvds  16226  lgsne0  16323  mul2sq  16401