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  948  bm1.1  2223  eqtr3  2258  elnelne1  2524  elnelne2  2525  morex  3010  reuss2  3513  reupick  3517  rabsneu  3780  invdisjrab  4119  opabss  4190  triun  4237  poirr  4447  wepo  4499  wetrep  4500  rexxfrd  4604  reg3exmidlemwe  4721  nnsuc  4758  fnfco  5559  fun11iun  5655  fnressn  5892  fvpr1g  5912  fvtp1g  5914  fvtp3g  5916  fvtp3  5919  f1mpt  5967  caovlem2d  6272  offval  6300  dfoprab3  6415  1stconst  6447  2ndconst  6448  poxp  6458  suppssrst  6491  suppssrgst  6492  tfrlemisucaccv  6586  tfr1onlemsucaccv  6602  tfrcllemsucaccv  6615  fiintim  7228  2omap  7308  pr1or2  7530  addclpi  7684  addnidpig  7693  reapmul1  8913  nnnn0addcl  9572  un0addcl  9575  un0mulcl  9576  zltnle  9669  nn0ge0div  9712  uzind3  9738  uzind4  9967  ltsubrp  10070  ltaddrp  10071  xrlttr  10176  xrltso  10177  xltnegi  10216  xaddnemnf  10238  xaddnepnf  10239  xaddcom  10242  xnegdi  10249  xsubge0  10262  fzind2  10636  qltnle  10656  qbtwnxr  10670  exp3vallem  10955  expp1  10961  expnegap0  10962  expcllem  10965  mulexpzap  10994  expaddzap  10998  expmulzap  11000  hashunlem  11222  cats1un  11471  reuccatpfxs1  11497  shftf  11573  sqrtdiv  11786  mulcn2  12056  summodclem2  12127  fsum3  12132  cvgratz  12277  prodmodclem2  12322  zproddc  12324  prodsnf  12337  dvdsflip  12596  dvdsfac  12605  bitsfzolem  12699  lcmgcdlem  12833  rpexp1i  12910  hashdvds  12977  hashgcdlem  12994  phisum  12997  pcqcl  13063  pcid  13081  ballotfilemfc0  13210  ballotfilemfcc  13211  ssnnctlemct  13315  issubmd  13758  grpinvnzcl  13854  mulgneg  13920  mulgnn0z  13929  01eq0ring  14469  lmss  15270  xmetrtri  15400  blssioo  15577  divcnap  15589  dedekindicc  15657  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvrecap  15737  dveflem  15750  pellexlem3  16007  lgsval3  16051  lgsdir2  16066  2sqlem6  16153  umgredg  16300  umgrpredgv  16302  umgredgne  16305  umgredgnlp  16307  usgredgppren  16352  edgssv2en  16354  uspgredg2vlem  16375  usgredg2vlem1  16377  uhgr0vsize0en  16390  wlkepvtx  16530  bj-bdfindes  16889  bj-findes  16921