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  943  bm1.1  2216  eqtr3  2251  elnelne1  2506  elnelne2  2507  morex  2990  reuss2  3487  reupick  3491  rabsneu  3744  invdisjrab  4082  opabss  4153  triun  4200  poirr  4404  wepo  4456  wetrep  4457  rexxfrd  4560  reg3exmidlemwe  4677  nnsuc  4714  fnfco  5511  fun11iun  5604  fnressn  5840  fvpr1g  5860  fvtp1g  5862  fvtp3g  5864  fvtp3  5867  f1mpt  5912  caovlem2d  6215  offval  6243  dfoprab3  6354  1stconst  6386  2ndconst  6387  poxp  6397  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  fiintim  7123  pr1or2  7399  addclpi  7547  addnidpig  7556  reapmul1  8775  nnnn0addcl  9432  un0addcl  9435  un0mulcl  9436  zltnle  9525  nn0ge0div  9567  uzind3  9593  uzind4  9822  ltsubrp  9925  ltaddrp  9926  xrlttr  10030  xrltso  10031  xltnegi  10070  xaddnemnf  10092  xaddnepnf  10093  xaddcom  10096  xnegdi  10103  xsubge0  10116  fzind2  10486  qltnle  10504  qbtwnxr  10518  exp3vallem  10803  expp1  10809  expnegap0  10810  expcllem  10813  mulexpzap  10842  expaddzap  10846  expmulzap  10848  hashunlem  11068  cats1un  11306  reuccatpfxs1  11332  shftf  11408  sqrtdiv  11620  mulcn2  11890  summodclem2  11961  fsum3  11966  cvgratz  12111  prodmodclem2  12156  zproddc  12158  prodsnf  12171  dvdsflip  12430  dvdsfac  12439  bitsfzolem  12533  lcmgcdlem  12667  rpexp1i  12744  hashdvds  12811  hashgcdlem  12828  phisum  12831  pcqcl  12897  pcid  12915  ssnnctlemct  13085  issubmd  13575  grpinvnzcl  13673  mulgneg  13745  mulgnn0z  13754  01eq0ring  14222  lmss  14989  xmetrtri  15119  blssioo  15296  divcnap  15308  dedekindicc  15376  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvrecap  15456  dveflem  15469  lgsval3  15766  lgsdir2  15781  2sqlem6  15868  umgredg  16015  umgrpredgv  16017  umgredgne  16020  umgredgnlp  16022  usgredgppren  16067  edgssv2en  16069  uspgredg2vlem  16090  usgredg2vlem1  16092  uhgr0vsize0en  16105  wlkepvtx  16245  bj-bdfindes  16595  bj-findes  16627  2omap  16645