Theorem sylbid 203

Description: A syllogism deduction.

Hypotheses

Ref	Expression
sylbid.1	|- (ph -> (ps <-> ch))
sylbid.2	|- (ph -> (ch -> th))

Assertion

Ref	Expression
sylbid	|- (ph -> (ps -> th))

Proof of Theorem sylbid

Step	Hyp	Ref	Expression
1		sylbid.1	. . 3 |- (ph -> (ps <-> ch))
2	1	biimpd 153	. 2 |- (ph -> (ps -> ch))
3		sylbid.2	. 2 |- (ph -> (ch -> th))
4	2, 3	syld 27	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  3imtr4d 545  hbsb4 1250  ax11eq 1365  ax11el 1366  vtoclegft 1859  sbciegft 1962  xp11 3482  foconst 3689  fvco 3780  isomin 3905  tfrlem5 3921  tz7.48lem 3961  oevn0 4160  oaass 4201  omword1 4210  omlimcl 4215  odi 4216  oneo 4218  oewordi 4224  oeworde 4226  th3qlem1 4320  dom2d 4410  fundmen 4434  unen 4440  ssfi 4547  ssfiOLD 4548  domfi 4549  domfiOLD 4550  isfinite2 4557  isfinite2OLD 4558  unfilem1 4560  noinfep 4650  r1tr 4664  r1ord3 4667  bndrank 4692  aceq3 4743  fodom 4808  alephordi 4885  mulcanpi 5039  addnidpi 5040  ltexpq 5092  ltbtwnpq 5096  genpss 5119  genpcd 5121  genpnmax 5122  mulclprlem 5133  distrlem1pr 5139  distrlem4pr 5142  distrlem5pr 5143  ltexprlem3 5156  ltexprlem6 5159  ltexpri 5161  reclem4pr 5171  cnegextlem1 5357  lelttrt 5535  ltletrt 5536  letrt 5537  xrlelttrt 5574  xrltletrt 5575  xrletrt 5576  xrrebndt 5580  ltleaddt 5657  divadddivt 5786  lemul1it 5839  lemul1itOLD 5840  squeeze0 5926  avglet 6046  suprleub 6061  supxrleub 6101  elnnz 6147  elnnz1 6157  zltp1let 6183  zextltt 6192  uzind2 6208  uzindOLD 6210  qrecclt 6274  qbtwnre 6279  monoord 6295  om2uzf1o 6302  elioc2t 6391  elico2t 6392  elicc2t 6393  icoshft 6409  icoshftf1oi 6410  indstr 6462  elfzlem 6474  fsequb 6524  expwordit 6604  sqlecant 6642  sqr0 6673  sqrlem6 6679  absnidt 6863  seq1bnd 6910  cau3ir 6915  caubnd 6926  facdivt 6942  facwordit 6944  faclbnd 6945  bccl2t 6971  fsum1s 7009  clm4le 7081  climunii 7098  climshft 7104  climge0 7112  climsup 7155  climcau 7156  serzf0 7169  ser1f0 7170  expcnvlem6 7232  cvgratlem2 7251  ivthlem1 7281  reeff1 7410  reeff1o 7426  tgtopt 7627  basgen2t 7638  bastop 7641  neips 7724  neindisj 7728  qdensere 7748  metxp 7831  bl2in 7840  rnblssm 7848  blss 7850  opnin 7866  metcnp 7884  blssioo 7910  tgioolem 7911  metelcls 7962  xplmi 7970  iscms2lem3 7988  lmcau 7993  cmsss 7994  bcthlem1 7996  bcthlem16 8011  bcthlem20 8015  bcthlem25 8020  ipasslem11 8496  psref 8645  pilem1 8666  sincosq3sgn 8701  sincosq4sgn 8702  efif1lem3 8727  efif1 8732  eff1i 8739  hlimunii 9103  chocuni 9167  projlem26 9206  h1de2ctlem 9473  spansneleq 9488  spansnsst 9489  normcant 9494  spansncv 9592  hmopidmchlem 10073  stadd3 10170  cvcon3t 10206  dmdbr5 10230  ssdmd2 10236  atom1d 10275  superpos 10276  cvexchlem 10290  atcv0eq 10301  atexcht 10303  atcvat4 10319  atdmd 10320  atmd2 10322  mdsymlem3 10327  mdsymlem5 10329  sumdmdlem 10340  cdjreu 10354  cdrci 10480  elioo1t3 10482  cnrsfin 10495  cnrscoa 10496  hmphsyma 10514  homcard 10525  set2elt 10531  iintlem1 10603  ismonb2 10711  icmpmon 10715  idmon 10716  isepib2 10721

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain