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  2219  eqtr3  2254  elnelne1  2518  elnelne2  2519  morex  3004  reuss2  3505  reupick  3509  rabsneu  3769  invdisjrab  4108  opabss  4179  triun  4226  poirr  4433  wepo  4485  wetrep  4486  rexxfrd  4589  reg3exmidlemwe  4706  nnsuc  4743  fnfco  5544  fun11iun  5640  fnressn  5875  fvpr1g  5895  fvtp1g  5897  fvtp3g  5899  fvtp3  5902  f1mpt  5950  caovlem2d  6255  offval  6283  dfoprab3  6398  1stconst  6430  2ndconst  6431  poxp  6441  suppssrst  6474  suppssrgst  6475  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  fiintim  7204  2omap  7282  pr1or2  7504  addclpi  7658  addnidpig  7667  reapmul1  8886  nnnn0addcl  9543  un0addcl  9546  un0mulcl  9547  zltnle  9640  nn0ge0div  9683  uzind3  9709  uzind4  9938  ltsubrp  10041  ltaddrp  10042  xrlttr  10147  xrltso  10148  xltnegi  10187  xaddnemnf  10209  xaddnepnf  10210  xaddcom  10213  xnegdi  10220  xsubge0  10233  fzind2  10607  qltnle  10627  qbtwnxr  10641  exp3vallem  10926  expp1  10932  expnegap0  10933  expcllem  10936  mulexpzap  10965  expaddzap  10969  expmulzap  10971  hashunlem  11193  cats1un  11438  reuccatpfxs1  11464  shftf  11540  sqrtdiv  11752  mulcn2  12022  summodclem2  12093  fsum3  12098  cvgratz  12243  prodmodclem2  12288  zproddc  12290  prodsnf  12303  dvdsflip  12562  dvdsfac  12571  bitsfzolem  12665  lcmgcdlem  12799  rpexp1i  12876  hashdvds  12943  hashgcdlem  12960  phisum  12963  pcqcl  13029  pcid  13047  ballotfilemfc0  13176  ballotfilemfcc  13177  ssnnctlemct  13281  issubmd  13729  grpinvnzcl  13827  mulgneg  13893  mulgnn0z  13902  01eq0ring  14434  lmss  15237  xmetrtri  15367  blssioo  15544  divcnap  15556  dedekindicc  15624  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvrecap  15704  dveflem  15717  pellexlem3  15973  lgsval3  16017  lgsdir2  16032  2sqlem6  16119  umgredg  16266  umgrpredgv  16268  umgredgne  16271  umgredgnlp  16273  usgredgppren  16318  edgssv2en  16320  uspgredg2vlem  16341  usgredg2vlem1  16343  uhgr0vsize0en  16356  wlkepvtx  16496  bj-bdfindes  16845  bj-findes  16877