Theorem syl2anb 275

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 268	. 2 |- ((ph /\ ch) -> th)
5	1, 4	sylan2b 271	1 |- ((ph /\ ta) -> th)

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  sylancb  395  reupick3  3216  difprsnss  3493  trin2  4659  imadiflem  4921  fnun  4948  fco  4999  f1co  5044  foco  5059  f1oun  5089  f1oco  5092  eqfunfv  5213  ftpg  5290  issmo  5844  tfrlem5  5871  ener  6195  domtr  6201  unen  6229  xpdom2  6241  axpre-lttrn  6768  axpre-mulgt0  6771  zmulcl  8073  qaddcl  8346  qmulcl  8348  rpaddcl  8381  rpmulcl  8382  rpdivcl  8383  xrltnsym  8484  xrlttri3  8488  ge0addcl  8620  ge0mulcl  8621  expclzaplem  8933  expge0  8945  expge1  8946