Theorem sylan2b 281

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
sylan2b.1	|- ( ph <-> ch )
sylan2b.2	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylan2b	|- ( ( ps /\ ph ) -> th )

Proof of Theorem sylan2b

Step	Hyp	Ref	Expression
1		sylan2b.1	. . 3 |- ( ph <-> ch )
2	1	biimpi 118	. 2 |- ( ph -> ch )
3		sylan2b.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan2 280	1 |- ( ( ps /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  syl2anb  285  dcor  876  bm1.1  2066  eqtr3  2100  morex  2776  reuss2  3244  reupick  3248  rabsneu  3465  opabss  3842  triun  3888  poirr  4062  wepo  4114  wetrep  4115  rexxfrd  4213  reg3exmidlemwe  4321  nnsuc  4356  fnfco  5085  fun11iun  5167  fnressn  5370  fvpr1g  5388  fvtp1g  5390  fvtp3g  5392  fvtp3  5395  f1mpt  5431  caovlem2d  5713  offval  5739  dfoprab3  5837  1stconst  5862  2ndconst  5863  poxp  5873  tfrlemisucaccv  5962  addclpi  6517  addnidpig  6526  reapmul1  7695  nnnn0addcl  8318  un0addcl  8321  un0mulcl  8322  zltnle  8397  nn0ge0div  8434  uzind3  8460  uzind4  8676  ltsubrp  8768  ltaddrp  8769  xrlttr  8870  xrltso  8871  xltnegi  8902  fzind2  9248  qltnle  9255  qbtwnxr  9266  expp1  9483  expnegap0  9484  expcllem  9487  mulexpzap  9516  expaddzap  9520  expmulzap  9522  shftf  9718  sqrtdiv  9928  mulcn2  10151  dvdsflip  10251  dvdsfac  10260  ialgrf  10427  lcmgcdlem  10459  rpexp1i  10533  bj-bdfindes  10744  bj-findes  10776