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  4196  triun  4244  poirr  4454  wepo  4506  wetrep  4507  rexxfrd  4611  reg3exmidlemwe  4728  nnsuc  4765  fnfco  5567  fun11iun  5663  fnressn  5904  fvpr1g  5924  fvtp1g  5926  fvtp3g  5928  fvtp3  5931  f1mpt  5980  caovlem2d  6285  offval  6314  dfoprab3  6429  1stconst  6461  2ndconst  6462  poxp  6472  suppssrst  6505  suppssrgst  6506  tfrlemisucaccv  6601  tfr1onlemsucaccv  6617  tfrcllemsucaccv  6630  fiintim  7244  2omap  7324  pr1or2  7546  addclpi  7700  addnidpig  7709  reapmul1  8931  nnnn0addcl  9604  un0addcl  9607  un0mulcl  9608  zltnle  9699  nn0ge0div  9742  uzind3  9769  uzind4  10003  ltsubrp  10107  ltaddrp  10108  xrlttr  10213  xrltso  10214  xltnegi  10253  xaddnemnf  10275  xaddnepnf  10276  xaddcom  10279  xnegdi  10286  xsubge0  10299  fzind2  10674  qltnle  10694  qbtwnxr  10708  exp3vallem  10997  expp1  11003  expnegap0  11004  expcllem  11007  mulexpzap  11036  expaddzap  11040  expmulzap  11042  hashunlem  11265  cats1un  11514  reuccatpfxs1  11540  shftf  11616  sqrtdiv  11829  mulcn2  12102  summodclem2  12173  fsum3  12178  cvgratz  12323  prodmodclem2  12368  zproddc  12370  prodsnf  12383  dvdsflip  12642  dvdsfac  12651  bitsfzolem  12745  lcmgcdlem  12879  rpexp1i  12957  hashdvds  13027  hashgcdlem  13044  phisum  13047  pcqcl  13113  pcid  13131  ballotfilemfc0  13289  ballotfilemfcc  13290  ssnnctlemct  13394  issubmd  13839  grpinvnzcl  13935  mulgneg  14001  mulgnn0z  14010  gsumunsnfd  14258  gsum2dfilem1  14270  gsum2dfilem2  14271  01eq0ring  14604  psrbaglefifi  15175  lmss  15489  xmetrtri  15619  blssioo  15796  divcnap  15808  dedekindicc  15876  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvrecap  15956  dveflem  15969  pellexlem3  16248  prmorcht  16299  lgsval3  16359  lgsdir2  16374  2sqlem6  16461  umgredg  16608  umgrpredgv  16610  umgredgne  16613  umgredgnlp  16615  usgredgppren  16660  edgssv2en  16662  uspgredg2vlem  16683  usgredg2vlem1  16685  uhgr0vsize0en  16698  wlkepvtx  16838  bj-bdfindes  17197  bj-findes  17229