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  3392  difprsnss  3695  trin2  4978  imadiflem  5250  fnun  5277  fco  5336  f1co  5388  foco  5403  f1oun  5435  f1oco  5438  eqfunfv  5571  ftpg  5652  issmo  6236  tfrlem5  6262  ener  6725  domtr  6731  unen  6762  xpdom2  6777  mapen  6792  pm54.43  7126  axpre-lttrn  7805  axpre-mulgt0  7808  zmulcl  9221  qaddcl  9545  qmulcl  9547  rpaddcl  9585  rpmulcl  9586  rpdivcl  9587  xrltnsym  9701  xrlttri3  9705  ge0addcl  9886  ge0mulcl  9887  ge0xaddcl  9888  expclzaplem  10447  expge0  10459  expge1  10460  hashfacen  10711  qredeu  11978  nn0gcdsq  12079  cnovex  12638  iscn2  12642  txuni  12705  txcn  12717