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  6258  1stconst  6288  2ndconst  6289  poxp  6299  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  fiintim  7001  addclpi  7413  addnidpig  7422  reapmul1  8641  nnnn0addcl  9298  un0addcl  9301  un0mulcl  9302  zltnle  9391  nn0ge0div  9432  uzind3  9458  uzind4  9681  ltsubrp  9784  ltaddrp  9785  xrlttr  9889  xrltso  9890  xltnegi  9929  xaddnemnf  9951  xaddnepnf  9952  xaddcom  9955  xnegdi  9962  xsubge0  9975  fzind2  10334  qltnle  10352  qbtwnxr  10366  exp3vallem  10651  expp1  10657  expnegap0  10658  expcllem  10661  mulexpzap  10690  expaddzap  10694  expmulzap  10696  hashunlem  10915  shftf  11014  sqrtdiv  11226  mulcn2  11496  summodclem2  11566  fsum3  11571  cvgratz  11716  prodmodclem2  11761  zproddc  11763  prodsnf  11776  dvdsflip  12035  dvdsfac  12044  bitsfzolem  12138  lcmgcdlem  12272  rpexp1i  12349  hashdvds  12416  hashgcdlem  12433  phisum  12436  pcqcl  12502  pcid  12520  ssnnctlemct  12690  issubmd  13178  grpinvnzcl  13276  mulgneg  13348  mulgnn0z  13357  01eq0ring  13823  lmss  14590  xmetrtri  14720  blssioo  14897  divcnap  14909  dedekindicc  14977  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvrecap  15057  dveflem  15070  lgsval3  15367  lgsdir2  15382  2sqlem6  15469  bj-bdfindes  15703  bj-findes  15735  2omap  15750