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  845  reupick3  3420  difprsnss  3730  trin2  5020  imadiflem  5295  fnun  5322  fco  5381  f1co  5433  foco  5448  f1oun  5481  f1oco  5484  eqfunfv  5618  ftpg  5700  issmo  6288  tfrlem5  6314  ener  6778  domtr  6784  unen  6815  xpdom2  6830  mapen  6845  pm54.43  7188  axpre-lttrn  7882  axpre-mulgt0  7885  zmulcl  9304  qaddcl  9633  qmulcl  9635  rpaddcl  9675  rpmulcl  9676  rpdivcl  9677  xrltnsym  9791  xrlttri3  9795  ge0addcl  9979  ge0mulcl  9980  ge0xaddcl  9981  expclzaplem  10541  expge0  10553  expge1  10554  hashfacen  10811  qredeu  12091  nn0gcdsq  12194  mul4sq  12386  cnovex  13627  iscn2  13631  txuni  13694  txcn  13706  lgsne0  14370  mul2sq  14383