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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  syl2anb  291  dcor  948  bm1.1  2223  eqtr3  2258  elnelne1  2524  elnelne2  2525  morex  3010  reuss2  3513  reupick  3517  rabsneu  3784  invdisjrab  4124  opabss  4195  triun  4242  poirr  4452  wepo  4504  wetrep  4505  rexxfrd  4609  reg3exmidlemwe  4726  nnsuc  4763  fnfco  5564  fun11iun  5660  fnressn  5901  fvpr1g  5921  fvtp1g  5923  fvtp3g  5925  fvtp3  5928  f1mpt  5977  caovlem2d  6282  offval  6310  dfoprab3  6425  1stconst  6457  2ndconst  6458  poxp  6468  suppssrst  6501  suppssrgst  6502  tfrlemisucaccv  6596  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  fiintim  7238  2omap  7318  pr1or2  7540  addclpi  7694  addnidpig  7703  reapmul1  8925  nnnn0addcl  9597  un0addcl  9600  un0mulcl  9601  zltnle  9694  nn0ge0div  9737  uzind3  9763  uzind4  9997  ltsubrp  10101  ltaddrp  10102  xrlttr  10207  xrltso  10208  xltnegi  10247  xaddnemnf  10269  xaddnepnf  10270  xaddcom  10273  xnegdi  10280  xsubge0  10293  fzind2  10668  qltnle  10688  qbtwnxr  10702  exp3vallem  10990  expp1  10996  expnegap0  10997  expcllem  11000  mulexpzap  11029  expaddzap  11033  expmulzap  11035  hashunlem  11258  cats1un  11507  reuccatpfxs1  11533  shftf  11609  sqrtdiv  11822  mulcn2  12094  summodclem2  12165  fsum3  12170  cvgratz  12315  prodmodclem2  12360  zproddc  12362  prodsnf  12375  dvdsflip  12634  dvdsfac  12643  bitsfzolem  12737  lcmgcdlem  12871  rpexp1i  12949  hashdvds  13019  hashgcdlem  13036  phisum  13039  pcqcl  13105  pcid  13123  ballotfilemfc0  13281  ballotfilemfcc  13282  ssnnctlemct  13386  issubmd  13830  grpinvnzcl  13926  mulgneg  13992  mulgnn0z  14001  01eq0ring  14545  lmss  15396  xmetrtri  15526  blssioo  15703  divcnap  15715  dedekindicc  15783  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvrecap  15863  dveflem  15876  pellexlem3  16150  lgsval3  16235  lgsdir2  16250  2sqlem6  16337  umgredg  16484  umgrpredgv  16486  umgredgne  16489  umgredgnlp  16491  usgredgppren  16536  edgssv2en  16538  uspgredg2vlem  16559  usgredg2vlem1  16561  uhgr0vsize0en  16574  wlkepvtx  16714  bj-bdfindes  17073  bj-findes  17105