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  3444  difprsnss  3756  trin2  5057  imadiflem  5333  fnun  5360  fco  5419  f1co  5471  foco  5487  f1oun  5520  f1oco  5523  eqfunfv  5660  ftpg  5742  issmo  6341  tfrlem5  6367  ener  6833  domtr  6839  unen  6870  xpdom2  6885  mapen  6902  pm54.43  7250  axpre-lttrn  7944  axpre-mulgt0  7947  zmulcl  9370  qaddcl  9700  qmulcl  9702  rpaddcl  9743  rpmulcl  9744  rpdivcl  9745  xrltnsym  9859  xrlttri3  9863  ge0addcl  10047  ge0mulcl  10048  ge0xaddcl  10049  expclzaplem  10634  expge0  10646  expge1  10647  hashfacen  10907  qredeu  12235  nn0gcdsq  12338  mul4sq  12532  cnovex  14364  iscn2  14368  txuni  14431  txcn  14443  lgsne0  15154  mul2sq  15203