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  5839  fvpr1g  5859  fvtp1g  5861  fvtp3g  5863  fvtp3  5866  f1mpt  5911  caovlem2d  6214  offval  6242  dfoprab3  6353  1stconst  6385  2ndconst  6386  poxp  6396  tfrlemisucaccv  6490  tfr1onlemsucaccv  6506  tfrcllemsucaccv  6519  fiintim  7122  pr1or2  7398  addclpi  7546  addnidpig  7555  reapmul1  8774  nnnn0addcl  9431  un0addcl  9434  un0mulcl  9435  zltnle  9524  nn0ge0div  9566  uzind3  9592  uzind4  9821  ltsubrp  9924  ltaddrp  9925  xrlttr  10029  xrltso  10030  xltnegi  10069  xaddnemnf  10091  xaddnepnf  10092  xaddcom  10095  xnegdi  10102  xsubge0  10115  fzind2  10484  qltnle  10502  qbtwnxr  10516  exp3vallem  10801  expp1  10807  expnegap0  10808  expcllem  10811  mulexpzap  10840  expaddzap  10844  expmulzap  10846  hashunlem  11066  cats1un  11301  reuccatpfxs1  11327  shftf  11390  sqrtdiv  11602  mulcn2  11872  summodclem2  11942  fsum3  11947  cvgratz  12092  prodmodclem2  12137  zproddc  12139  prodsnf  12152  dvdsflip  12411  dvdsfac  12420  bitsfzolem  12514  lcmgcdlem  12648  rpexp1i  12725  hashdvds  12792  hashgcdlem  12809  phisum  12812  pcqcl  12878  pcid  12896  ssnnctlemct  13066  issubmd  13556  grpinvnzcl  13654  mulgneg  13726  mulgnn0z  13735  01eq0ring  14202  lmss  14969  xmetrtri  15099  blssioo  15276  divcnap  15288  dedekindicc  15356  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvrecap  15436  dveflem  15449  lgsval3  15746  lgsdir2  15761  2sqlem6  15848  umgredg  15995  umgrpredgv  15997  umgredgne  16000  umgredgnlp  16002  usgredgppren  16047  edgssv2en  16049  uspgredg2vlem  16070  usgredg2vlem1  16072  uhgr0vsize0en  16085  wlkepvtx  16225  bj-bdfindes  16544  bj-findes  16576  2omap  16594