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 )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylancb  418  stdcndc  850  reupick3  3489  difprsnss  3806  trin2  5120  fundif  5365  imadiflem  5400  fnun  5429  fco  5491  f1co  5545  foco  5561  f1oun  5594  f1oco  5597  eqfunfv  5739  ftpg  5827  issmo  6440  tfrlem5  6466  ener  6939  domtr  6945  unen  6977  xpdom2  6998  mapen  7015  pm54.43  7374  axpre-lttrn  8082  axpre-mulgt0  8085  zmulcl  9511  qaddcl  9842  qmulcl  9844  rpaddcl  9885  rpmulcl  9886  rpdivcl  9887  xrltnsym  10001  xrlttri3  10005  ge0addcl  10189  ge0mulcl  10190  ge0xaddcl  10191  expclzaplem  10797  expge0  10809  expge1  10810  hashfacen  11071  qredeu  12634  nn0gcdsq  12737  mul4sq  12932  cnovex  14885  iscn2  14889  txuni  14952  txcn  14964  lgsne0  15732  mul2sq  15810