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  2178  eqtr3  2213  elnelne1  2468  elnelne2  2469  morex  2945  reuss2  3440  reupick  3444  rabsneu  3692  opabss  4094  triun  4141  poirr  4339  wepo  4391  wetrep  4392  rexxfrd  4495  reg3exmidlemwe  4612  nnsuc  4649  fnfco  5429  fun11iun  5522  fnressn  5745  fvpr1g  5765  fvtp1g  5767  fvtp3g  5769  fvtp3  5772  f1mpt  5815  caovlem2d  6113  offval  6140  dfoprab3  6246  1stconst  6276  2ndconst  6277  poxp  6287  tfrlemisucaccv  6380  tfr1onlemsucaccv  6396  tfrcllemsucaccv  6409  fiintim  6987  addclpi  7389  addnidpig  7398  reapmul1  8616  nnnn0addcl  9273  un0addcl  9276  un0mulcl  9277  zltnle  9366  nn0ge0div  9407  uzind3  9433  uzind4  9656  ltsubrp  9759  ltaddrp  9760  xrlttr  9864  xrltso  9865  xltnegi  9904  xaddnemnf  9926  xaddnepnf  9927  xaddcom  9930  xnegdi  9937  xsubge0  9950  fzind2  10309  qltnle  10316  qbtwnxr  10329  exp3vallem  10614  expp1  10620  expnegap0  10621  expcllem  10624  mulexpzap  10653  expaddzap  10657  expmulzap  10659  hashunlem  10878  shftf  10977  sqrtdiv  11189  mulcn2  11458  summodclem2  11528  fsum3  11533  cvgratz  11678  prodmodclem2  11723  zproddc  11725  prodsnf  11738  dvdsflip  11996  dvdsfac  12005  lcmgcdlem  12218  rpexp1i  12295  hashdvds  12362  hashgcdlem  12379  phisum  12381  pcqcl  12447  pcid  12465  ssnnctlemct  12606  issubmd  13049  grpinvnzcl  13147  mulgneg  13213  mulgnn0z  13222  01eq0ring  13688  lmss  14425  xmetrtri  14555  blssioo  14732  divcnap  14744  dedekindicc  14812  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvrecap  14892  dveflem  14905  lgsval3  15175  lgsdir2  15190  2sqlem6  15277  bj-bdfindes  15511  bj-findes  15543