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  941  bm1.1  2214  eqtr3  2249  elnelne1  2504  elnelne2  2505  morex  2987  reuss2  3484  reupick  3488  rabsneu  3739  invdisjrab  4076  opabss  4147  triun  4194  poirr  4397  wepo  4449  wetrep  4450  rexxfrd  4553  reg3exmidlemwe  4670  nnsuc  4707  fnfco  5499  fun11iun  5592  fnressn  5824  fvpr1g  5844  fvtp1g  5846  fvtp3g  5848  fvtp3  5851  f1mpt  5894  caovlem2d  6197  offval  6224  dfoprab3  6335  1stconst  6365  2ndconst  6366  poxp  6376  tfrlemisucaccv  6469  tfr1onlemsucaccv  6485  tfrcllemsucaccv  6498  fiintim  7089  pr1or2  7363  addclpi  7510  addnidpig  7519  reapmul1  8738  nnnn0addcl  9395  un0addcl  9398  un0mulcl  9399  zltnle  9488  nn0ge0div  9530  uzind3  9556  uzind4  9779  ltsubrp  9882  ltaddrp  9883  xrlttr  9987  xrltso  9988  xltnegi  10027  xaddnemnf  10049  xaddnepnf  10050  xaddcom  10053  xnegdi  10060  xsubge0  10073  fzind2  10440  qltnle  10458  qbtwnxr  10472  exp3vallem  10757  expp1  10763  expnegap0  10764  expcllem  10767  mulexpzap  10796  expaddzap  10800  expmulzap  10802  hashunlem  11021  cats1un  11248  reuccatpfxs1  11274  shftf  11336  sqrtdiv  11548  mulcn2  11818  summodclem2  11888  fsum3  11893  cvgratz  12038  prodmodclem2  12083  zproddc  12085  prodsnf  12098  dvdsflip  12357  dvdsfac  12366  bitsfzolem  12460  lcmgcdlem  12594  rpexp1i  12671  hashdvds  12738  hashgcdlem  12755  phisum  12758  pcqcl  12824  pcid  12842  ssnnctlemct  13012  issubmd  13502  grpinvnzcl  13600  mulgneg  13672  mulgnn0z  13681  01eq0ring  14147  lmss  14914  xmetrtri  15044  blssioo  15221  divcnap  15233  dedekindicc  15301  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvrecap  15381  dveflem  15394  lgsval3  15691  lgsdir2  15706  2sqlem6  15793  umgredg  15937  umgrpredgv  15939  umgredgne  15942  umgredgnlp  15944  usgredgppren  15989  edgssv2en  15991  uspgredg2vlem  16012  usgredg2vlem1  16014  bj-bdfindes  16270  bj-findes  16302  2omap  16318