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  944  bm1.1  2216  eqtr3  2251  elnelne1  2507  elnelne2  2508  morex  2991  reuss2  3489  reupick  3493  rabsneu  3748  invdisjrab  4087  opabss  4158  triun  4205  poirr  4410  wepo  4462  wetrep  4463  rexxfrd  4566  reg3exmidlemwe  4683  nnsuc  4720  fnfco  5519  fun11iun  5613  fnressn  5848  fvpr1g  5868  fvtp1g  5870  fvtp3g  5872  fvtp3  5875  f1mpt  5922  caovlem2d  6225  offval  6252  dfoprab3  6363  1stconst  6395  2ndconst  6396  poxp  6406  suppssrst  6439  suppssrgst  6440  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  fiintim  7166  pr1or2  7442  addclpi  7590  addnidpig  7599  reapmul1  8817  nnnn0addcl  9474  un0addcl  9477  un0mulcl  9478  zltnle  9569  nn0ge0div  9611  uzind3  9637  uzind4  9866  ltsubrp  9969  ltaddrp  9970  xrlttr  10074  xrltso  10075  xltnegi  10114  xaddnemnf  10136  xaddnepnf  10137  xaddcom  10140  xnegdi  10147  xsubge0  10160  fzind2  10531  qltnle  10549  qbtwnxr  10563  exp3vallem  10848  expp1  10854  expnegap0  10855  expcllem  10858  mulexpzap  10887  expaddzap  10891  expmulzap  10893  hashunlem  11113  cats1un  11351  reuccatpfxs1  11377  shftf  11453  sqrtdiv  11665  mulcn2  11935  summodclem2  12006  fsum3  12011  cvgratz  12156  prodmodclem2  12201  zproddc  12203  prodsnf  12216  dvdsflip  12475  dvdsfac  12484  bitsfzolem  12578  lcmgcdlem  12712  rpexp1i  12789  hashdvds  12856  hashgcdlem  12873  phisum  12876  pcqcl  12942  pcid  12960  ssnnctlemct  13130  issubmd  13620  grpinvnzcl  13718  mulgneg  13790  mulgnn0z  13799  01eq0ring  14267  lmss  15040  xmetrtri  15170  blssioo  15347  divcnap  15359  dedekindicc  15427  dvidlemap  15485  dvidrelem  15486  dvidsslem  15487  dvrecap  15507  dveflem  15520  pellexlem3  15776  lgsval3  15820  lgsdir2  15835  2sqlem6  15922  umgredg  16069  umgrpredgv  16071  umgredgne  16074  umgredgnlp  16076  usgredgppren  16121  edgssv2en  16123  uspgredg2vlem  16144  usgredg2vlem1  16146  uhgr0vsize0en  16159  wlkepvtx  16299  bj-bdfindes  16648  bj-findes  16680  2omap  16698