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  2190  eqtr3  2225  elnelne1  2480  elnelne2  2481  morex  2957  reuss2  3453  reupick  3457  rabsneu  3706  opabss  4108  triun  4155  poirr  4354  wepo  4406  wetrep  4407  rexxfrd  4510  reg3exmidlemwe  4627  nnsuc  4664  fnfco  5450  fun11iun  5543  fnressn  5770  fvpr1g  5790  fvtp1g  5792  fvtp3g  5794  fvtp3  5797  f1mpt  5840  caovlem2d  6139  offval  6166  dfoprab3  6277  1stconst  6307  2ndconst  6308  poxp  6318  tfrlemisucaccv  6411  tfr1onlemsucaccv  6427  tfrcllemsucaccv  6440  fiintim  7028  addclpi  7440  addnidpig  7449  reapmul1  8668  nnnn0addcl  9325  un0addcl  9328  un0mulcl  9329  zltnle  9418  nn0ge0div  9460  uzind3  9486  uzind4  9709  ltsubrp  9812  ltaddrp  9813  xrlttr  9917  xrltso  9918  xltnegi  9957  xaddnemnf  9979  xaddnepnf  9980  xaddcom  9983  xnegdi  9990  xsubge0  10003  fzind2  10368  qltnle  10386  qbtwnxr  10400  exp3vallem  10685  expp1  10691  expnegap0  10692  expcllem  10695  mulexpzap  10724  expaddzap  10728  expmulzap  10730  hashunlem  10949  shftf  11141  sqrtdiv  11353  mulcn2  11623  summodclem2  11693  fsum3  11698  cvgratz  11843  prodmodclem2  11888  zproddc  11890  prodsnf  11903  dvdsflip  12162  dvdsfac  12171  bitsfzolem  12265  lcmgcdlem  12399  rpexp1i  12476  hashdvds  12543  hashgcdlem  12560  phisum  12563  pcqcl  12629  pcid  12647  ssnnctlemct  12817  issubmd  13306  grpinvnzcl  13404  mulgneg  13476  mulgnn0z  13485  01eq0ring  13951  lmss  14718  xmetrtri  14848  blssioo  15025  divcnap  15037  dedekindicc  15105  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvrecap  15185  dveflem  15198  lgsval3  15495  lgsdir2  15510  2sqlem6  15597  bj-bdfindes  15885  bj-findes  15917  2omap  15932