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  846  reupick3  3457  difprsnss  3770  trin2  5073  fundif  5317  imadiflem  5352  fnun  5381  fco  5440  f1co  5492  foco  5508  f1oun  5541  f1oco  5544  eqfunfv  5681  ftpg  5767  issmo  6373  tfrlem5  6399  ener  6870  domtr  6876  unen  6907  xpdom2  6925  mapen  6942  pm54.43  7297  axpre-lttrn  7996  axpre-mulgt0  7999  zmulcl  9425  qaddcl  9755  qmulcl  9757  rpaddcl  9798  rpmulcl  9799  rpdivcl  9800  xrltnsym  9914  xrlttri3  9918  ge0addcl  10102  ge0mulcl  10103  ge0xaddcl  10104  expclzaplem  10706  expge0  10718  expge1  10719  hashfacen  10979  qredeu  12361  nn0gcdsq  12464  mul4sq  12659  cnovex  14610  iscn2  14614  txuni  14677  txcn  14689  lgsne0  15457  mul2sq  15535