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  938  bm1.1  2192  eqtr3  2227  elnelne1  2482  elnelne2  2483  morex  2964  reuss2  3461  reupick  3465  rabsneu  3716  invdisjrab  4053  opabss  4124  triun  4171  poirr  4372  wepo  4424  wetrep  4425  rexxfrd  4528  reg3exmidlemwe  4645  nnsuc  4682  fnfco  5472  fun11iun  5565  fnressn  5793  fvpr1g  5813  fvtp1g  5815  fvtp3g  5817  fvtp3  5820  f1mpt  5863  caovlem2d  6162  offval  6189  dfoprab3  6300  1stconst  6330  2ndconst  6331  poxp  6341  tfrlemisucaccv  6434  tfr1onlemsucaccv  6450  tfrcllemsucaccv  6463  fiintim  7054  pr1or2  7328  addclpi  7475  addnidpig  7484  reapmul1  8703  nnnn0addcl  9360  un0addcl  9363  un0mulcl  9364  zltnle  9453  nn0ge0div  9495  uzind3  9521  uzind4  9744  ltsubrp  9847  ltaddrp  9848  xrlttr  9952  xrltso  9953  xltnegi  9992  xaddnemnf  10014  xaddnepnf  10015  xaddcom  10018  xnegdi  10025  xsubge0  10038  fzind2  10405  qltnle  10423  qbtwnxr  10437  exp3vallem  10722  expp1  10728  expnegap0  10729  expcllem  10732  mulexpzap  10761  expaddzap  10765  expmulzap  10767  hashunlem  10986  cats1un  11212  reuccatpfxs1  11238  shftf  11256  sqrtdiv  11468  mulcn2  11738  summodclem2  11808  fsum3  11813  cvgratz  11958  prodmodclem2  12003  zproddc  12005  prodsnf  12018  dvdsflip  12277  dvdsfac  12286  bitsfzolem  12380  lcmgcdlem  12514  rpexp1i  12591  hashdvds  12658  hashgcdlem  12675  phisum  12678  pcqcl  12744  pcid  12762  ssnnctlemct  12932  issubmd  13421  grpinvnzcl  13519  mulgneg  13591  mulgnn0z  13600  01eq0ring  14066  lmss  14833  xmetrtri  14963  blssioo  15140  divcnap  15152  dedekindicc  15220  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvrecap  15300  dveflem  15313  lgsval3  15610  lgsdir2  15625  2sqlem6  15712  umgredg  15849  umgrpredgv  15851  umgredgne  15854  umgredgnlp  15856  bj-bdfindes  16084  bj-findes  16116  2omap  16132