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  835  reupick3  3407  difprsnss  3711  trin2  4995  imadiflem  5267  fnun  5294  fco  5353  f1co  5405  foco  5420  f1oun  5452  f1oco  5455  eqfunfv  5588  ftpg  5669  issmo  6256  tfrlem5  6282  ener  6745  domtr  6751  unen  6782  xpdom2  6797  mapen  6812  pm54.43  7146  axpre-lttrn  7825  axpre-mulgt0  7828  zmulcl  9244  qaddcl  9573  qmulcl  9575  rpaddcl  9613  rpmulcl  9614  rpdivcl  9615  xrltnsym  9729  xrlttri3  9733  ge0addcl  9917  ge0mulcl  9918  ge0xaddcl  9919  expclzaplem  10479  expge0  10491  expge1  10492  hashfacen  10749  qredeu  12029  nn0gcdsq  12132  mul4sq  12324  cnovex  12836  iscn2  12840  txuni  12903  txcn  12915  lgsne0  13579  mul2sq  13592