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  850  reupick3  3489  difprsnss  3805  trin2  5119  fundif  5364  imadiflem  5399  fnun  5428  fco  5488  f1co  5542  foco  5558  f1oun  5591  f1oco  5594  eqfunfv  5736  ftpg  5822  issmo  6432  tfrlem5  6458  ener  6929  domtr  6935  unen  6967  xpdom2  6986  mapen  7003  pm54.43  7359  axpre-lttrn  8067  axpre-mulgt0  8070  zmulcl  9496  qaddcl  9826  qmulcl  9828  rpaddcl  9869  rpmulcl  9870  rpdivcl  9871  xrltnsym  9985  xrlttri3  9989  ge0addcl  10173  ge0mulcl  10174  ge0xaddcl  10175  expclzaplem  10780  expge0  10792  expge1  10793  hashfacen  11053  qredeu  12614  nn0gcdsq  12717  mul4sq  12912  cnovex  14864  iscn2  14868  txuni  14931  txcn  14943  lgsne0  15711  mul2sq  15789