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  7319  pr1or2  7541  addclpi  7695  addnidpig  7704  reapmul1  8926  nnnn0addcl  9598  un0addcl  9601  un0mulcl  9602  zltnle  9695  nn0ge0div  9738  uzind3  9764  uzind4  9998  ltsubrp  10102  ltaddrp  10103  xrlttr  10208  xrltso  10209  xltnegi  10248  xaddnemnf  10270  xaddnepnf  10271  xaddcom  10274  xnegdi  10281  xsubge0  10294  fzind2  10669  qltnle  10689  qbtwnxr  10703  exp3vallem  10992  expp1  10998  expnegap0  10999  expcllem  11002  mulexpzap  11031  expaddzap  11035  expmulzap  11037  hashunlem  11260  cats1un  11509  reuccatpfxs1  11535  shftf  11611  sqrtdiv  11824  mulcn2  12097  summodclem2  12168  fsum3  12173  cvgratz  12318  prodmodclem2  12363  zproddc  12365  prodsnf  12378  dvdsflip  12637  dvdsfac  12646  bitsfzolem  12740  lcmgcdlem  12874  rpexp1i  12952  hashdvds  13022  hashgcdlem  13039  phisum  13042  pcqcl  13108  pcid  13126  ballotfilemfc0  13284  ballotfilemfcc  13285  ssnnctlemct  13389  issubmd  13834  grpinvnzcl  13930  mulgneg  13996  mulgnn0z  14005  01eq0ring  14580  psrbaglefifi  15147  lmss  15438  xmetrtri  15568  blssioo  15745  divcnap  15757  dedekindicc  15825  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvrecap  15905  dveflem  15918  pellexlem3  16192  prmorcht  16243  lgsval3  16303  lgsdir2  16318  2sqlem6  16405  umgredg  16552  umgrpredgv  16554  umgredgne  16557  umgredgnlp  16559  usgredgppren  16604  edgssv2en  16606  uspgredg2vlem  16627  usgredg2vlem1  16629  uhgr0vsize0en  16642  wlkepvtx  16782  bj-bdfindes  17141  bj-findes  17173