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  852  reupick3  3492  difprsnss  3811  trin2  5128  fundif  5374  imadiflem  5409  fnun  5438  fco  5500  f1co  5554  foco  5570  f1oun  5603  f1oco  5606  eqfunfv  5749  ftpg  5837  issmo  6453  tfrlem5  6479  ener  6952  domtr  6958  unen  6990  xpdom2  7014  mapen  7031  pm54.43  7394  axpre-lttrn  8103  axpre-mulgt0  8106  zmulcl  9532  qaddcl  9868  qmulcl  9870  rpaddcl  9911  rpmulcl  9912  rpdivcl  9913  xrltnsym  10027  xrlttri3  10031  ge0addcl  10215  ge0mulcl  10216  ge0xaddcl  10217  expclzaplem  10824  expge0  10836  expge1  10837  hashfacen  11099  qredeu  12668  nn0gcdsq  12771  mul4sq  12966  cnovex  14919  iscn2  14923  txuni  14986  txcn  14998  lgsne0  15766  mul2sq  15844