Theorem sylan2b 287

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 120	. 2 |- ( ph -> ch )
3		sylan2b.2	. 2 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan2 286	1 |- ( ( ps /\ ph ) -> 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:  syl2anb  291  dcor  937  bm1.1  2181  eqtr3  2216  elnelne1  2471  elnelne2  2472  morex  2948  reuss2  3444  reupick  3448  rabsneu  3696  opabss  4098  triun  4145  poirr  4343  wepo  4395  wetrep  4396  rexxfrd  4499  reg3exmidlemwe  4616  nnsuc  4653  fnfco  5435  fun11iun  5528  fnressn  5751  fvpr1g  5771  fvtp1g  5773  fvtp3g  5775  fvtp3  5778  f1mpt  5821  caovlem2d  6120  offval  6147  dfoprab3  6253  1stconst  6283  2ndconst  6284  poxp  6294  tfrlemisucaccv  6387  tfr1onlemsucaccv  6403  tfrcllemsucaccv  6416  fiintim  6996  addclpi  7399  addnidpig  7408  reapmul1  8627  nnnn0addcl  9284  un0addcl  9287  un0mulcl  9288  zltnle  9377  nn0ge0div  9418  uzind3  9444  uzind4  9667  ltsubrp  9770  ltaddrp  9771  xrlttr  9875  xrltso  9876  xltnegi  9915  xaddnemnf  9937  xaddnepnf  9938  xaddcom  9941  xnegdi  9948  xsubge0  9961  fzind2  10320  qltnle  10338  qbtwnxr  10352  exp3vallem  10637  expp1  10643  expnegap0  10644  expcllem  10647  mulexpzap  10676  expaddzap  10680  expmulzap  10682  hashunlem  10901  shftf  11000  sqrtdiv  11212  mulcn2  11482  summodclem2  11552  fsum3  11557  cvgratz  11702  prodmodclem2  11747  zproddc  11749  prodsnf  11762  dvdsflip  12021  dvdsfac  12030  bitsfzolem  12124  lcmgcdlem  12258  rpexp1i  12335  hashdvds  12402  hashgcdlem  12419  phisum  12422  pcqcl  12488  pcid  12506  ssnnctlemct  12676  issubmd  13153  grpinvnzcl  13251  mulgneg  13317  mulgnn0z  13326  01eq0ring  13792  lmss  14529  xmetrtri  14659  blssioo  14836  divcnap  14848  dedekindicc  14916  dvidlemap  14974  dvidrelem  14975  dvidsslem  14976  dvrecap  14996  dveflem  15009  lgsval3  15306  lgsdir2  15321  2sqlem6  15408  bj-bdfindes  15642  bj-findes  15674  2omap  15689