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  2174  eqtr3  2209  elnelne1  2464  elnelne2  2465  morex  2936  reuss2  3430  reupick  3434  rabsneu  3680  opabss  4082  triun  4129  poirr  4325  wepo  4377  wetrep  4378  rexxfrd  4481  reg3exmidlemwe  4596  nnsuc  4633  fnfco  5409  fun11iun  5501  fnressn  5723  fvpr1g  5743  fvtp1g  5745  fvtp3g  5747  fvtp3  5750  f1mpt  5793  caovlem2d  6089  offval  6114  dfoprab3  6216  1stconst  6246  2ndconst  6247  poxp  6257  tfrlemisucaccv  6350  tfr1onlemsucaccv  6366  tfrcllemsucaccv  6379  fiintim  6957  addclpi  7356  addnidpig  7365  reapmul1  8582  nnnn0addcl  9236  un0addcl  9239  un0mulcl  9240  zltnle  9329  nn0ge0div  9370  uzind3  9396  uzind4  9618  ltsubrp  9720  ltaddrp  9721  xrlttr  9825  xrltso  9826  xltnegi  9865  xaddnemnf  9887  xaddnepnf  9888  xaddcom  9891  xnegdi  9898  xsubge0  9911  fzind2  10269  qltnle  10276  qbtwnxr  10288  exp3vallem  10552  expp1  10558  expnegap0  10559  expcllem  10562  mulexpzap  10591  expaddzap  10595  expmulzap  10597  hashunlem  10816  shftf  10871  sqrtdiv  11083  mulcn2  11352  summodclem2  11422  fsum3  11427  cvgratz  11572  prodmodclem2  11617  zproddc  11619  prodsnf  11632  dvdsflip  11889  dvdsfac  11898  lcmgcdlem  12109  rpexp1i  12186  hashdvds  12253  hashgcdlem  12270  phisum  12272  pcqcl  12338  pcid  12356  ssnnctlemct  12497  issubmd  12926  grpinvnzcl  13016  mulgneg  13080  mulgnn0z  13089  01eq0ring  13536  lmss  14203  xmetrtri  14333  blssioo  14502  divcnap  14512  dedekindicc  14568  dvidlemap  14617  dvrecap  14634  dveflem  14644  lgsval3  14877  lgsdir2  14892  2sqlem6  14925  bj-bdfindes  15159  bj-findes  15191