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  3443  reupick  3447  rabsneu  3695  opabss  4097  triun  4144  poirr  4342  wepo  4394  wetrep  4395  rexxfrd  4498  reg3exmidlemwe  4615  nnsuc  4652  fnfco  5432  fun11iun  5525  fnressn  5748  fvpr1g  5768  fvtp1g  5770  fvtp3g  5772  fvtp3  5775  f1mpt  5818  caovlem2d  6116  offval  6143  dfoprab3  6249  1stconst  6279  2ndconst  6280  poxp  6290  tfrlemisucaccv  6383  tfr1onlemsucaccv  6399  tfrcllemsucaccv  6412  fiintim  6992  addclpi  7394  addnidpig  7403  reapmul1  8622  nnnn0addcl  9279  un0addcl  9282  un0mulcl  9283  zltnle  9372  nn0ge0div  9413  uzind3  9439  uzind4  9662  ltsubrp  9765  ltaddrp  9766  xrlttr  9870  xrltso  9871  xltnegi  9910  xaddnemnf  9932  xaddnepnf  9933  xaddcom  9936  xnegdi  9943  xsubge0  9956  fzind2  10315  qltnle  10333  qbtwnxr  10347  exp3vallem  10632  expp1  10638  expnegap0  10639  expcllem  10642  mulexpzap  10671  expaddzap  10675  expmulzap  10677  hashunlem  10896  shftf  10995  sqrtdiv  11207  mulcn2  11477  summodclem2  11547  fsum3  11552  cvgratz  11697  prodmodclem2  11742  zproddc  11744  prodsnf  11757  dvdsflip  12016  dvdsfac  12025  bitsfzolem  12118  lcmgcdlem  12245  rpexp1i  12322  hashdvds  12389  hashgcdlem  12406  phisum  12409  pcqcl  12475  pcid  12493  ssnnctlemct  12663  issubmd  13106  grpinvnzcl  13204  mulgneg  13270  mulgnn0z  13279  01eq0ring  13745  lmss  14482  xmetrtri  14612  blssioo  14789  divcnap  14801  dedekindicc  14869  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvrecap  14949  dveflem  14962  lgsval3  15259  lgsdir2  15274  2sqlem6  15361  bj-bdfindes  15595  bj-findes  15627