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  415  stdcndc  831  reupick3  3366  difprsnss  3666  trin2  4938  imadiflem  5210  fnun  5237  fco  5296  f1co  5348  foco  5363  f1oun  5395  f1oco  5398  eqfunfv  5531  ftpg  5612  issmo  6193  tfrlem5  6219  ener  6681  domtr  6687  unen  6718  xpdom2  6733  mapen  6748  pm54.43  7063  axpre-lttrn  7716  axpre-mulgt0  7719  zmulcl  9131  qaddcl  9454  qmulcl  9456  rpaddcl  9494  rpmulcl  9495  rpdivcl  9496  xrltnsym  9609  xrlttri3  9613  ge0addcl  9794  ge0mulcl  9795  ge0xaddcl  9796  expclzaplem  10348  expge0  10360  expge1  10361  hashfacen  10611  qredeu  11814  nn0gcdsq  11914  cnovex  12404  iscn2  12408  txuni  12471  txcn  12483