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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  syl2anb  291  dcor  948  bm1.1  2223  eqtr3  2258  elnelne1  2524  elnelne2  2525  morex  3010  reuss2  3513  reupick  3517  rabsneu  3784  invdisjrab  4124  opabss  4195  triun  4242  poirr  4452  wepo  4504  wetrep  4505  rexxfrd  4609  reg3exmidlemwe  4726  nnsuc  4763  fnfco  5564  fun11iun  5660  fnressn  5901  fvpr1g  5921  fvtp1g  5923  fvtp3g  5925  fvtp3  5928  f1mpt  5977  caovlem2d  6282  offval  6310  dfoprab3  6425  1stconst  6457  2ndconst  6458  poxp  6468  suppssrst  6501  suppssrgst  6502  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  fiintim  7238  2omap  7318  pr1or2  7540  addclpi  7694  addnidpig  7703  reapmul1  8923  nnnn0addcl  9593  un0addcl  9596  un0mulcl  9597  zltnle  9690  nn0ge0div  9733  uzind3  9759  uzind4  9988  ltsubrp  10091  ltaddrp  10092  xrlttr  10197  xrltso  10198  xltnegi  10237  xaddnemnf  10259  xaddnepnf  10260  xaddcom  10263  xnegdi  10270  xsubge0  10283  fzind2  10658  qltnle  10678  qbtwnxr  10692  exp3vallem  10977  expp1  10983  expnegap0  10984  expcllem  10987  mulexpzap  11016  expaddzap  11020  expmulzap  11022  hashunlem  11244  cats1un  11493  reuccatpfxs1  11519  shftf  11595  sqrtdiv  11808  mulcn2  12078  summodclem2  12149  fsum3  12154  cvgratz  12299  prodmodclem2  12344  zproddc  12346  prodsnf  12359  dvdsflip  12618  dvdsfac  12627  bitsfzolem  12721  lcmgcdlem  12855  rpexp1i  12932  hashdvds  12999  hashgcdlem  13016  phisum  13019  pcqcl  13085  pcid  13103  ballotfilemfc0  13232  ballotfilemfcc  13233  ssnnctlemct  13337  issubmd  13781  grpinvnzcl  13877  mulgneg  13943  mulgnn0z  13952  01eq0ring  14496  lmss  15347  xmetrtri  15477  blssioo  15654  divcnap  15666  dedekindicc  15734  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvrecap  15814  dveflem  15827  pellexlem3  16093  lgsval3  16137  lgsdir2  16152  2sqlem6  16239  umgredg  16386  umgrpredgv  16388  umgredgne  16391  umgredgnlp  16393  usgredgppren  16438  edgssv2en  16440  uspgredg2vlem  16461  usgredg2vlem1  16463  uhgr0vsize0en  16476  wlkepvtx  16616  bj-bdfindes  16975  bj-findes  17007