Theorem sylan2b 271

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 113	. 2 |- ( ph -> ch )
3		sylan2b.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan2 270	1 |- ( ( ps /\ ph ) -> 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:  syl2anb  275  dcor  843  bm1.1  2025  eqtr3  2059  morex  2725  reuss2  3217  reupick  3221  rabsneu  3443  opabss  3821  triun  3867  poirr  4044  wepo  4096  wetrep  4097  rexxfrd  4195  reg3exmidlemwe  4303  nnsuc  4338  fnfco  5065  fun11iun  5147  fnressn  5349  fvpr1g  5367  fvtp1g  5369  fvtp3g  5371  fvtp3  5374  f1mpt  5410  caovlem2d  5693  offval  5719  dfoprab3  5817  1stconst  5842  2ndconst  5843  poxp  5853  tfrlemisucaccv  5939  addclpi  6425  addnidpig  6434  reapmul1  7586  nnnn0addcl  8212  un0addcl  8215  un0mulcl  8216  zltnle  8291  nn0ge0div  8327  uzind3  8351  uzind4  8531  ltsubrp  8617  ltaddrp  8618  xrlttr  8716  xrltso  8717  xltnegi  8748  fzind2  9095  qltnle  9101  expp1  9262  expnegap0  9263  expcllem  9266  mulexpzap  9295  expaddzap  9299  expmulzap  9301  shftf  9431  sqrtdiv  9640  mulcn2  9833  ialgrf  9884  bj-bdfindes  10074  bj-findes  10106