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 543  hbsb4 1248  ax11eq 1363  ax11el 1364  vtoclegft 1856  sbciegft 1959  xp11 3476  foconst 3683  fvco 3774  isomin 3899  tfrlem5 3915  tz7.48lem 3955  oevn0 4154  oaass 4195  omword1 4204  omlimcl 4209  odi 4210  oneo 4212  oewordi 4218  oeworde 4220  th3qlem1 4314  dom2d 4404  fundmen 4428  unen 4434  onfinOLD 4520  ssfi 4537  ssfiOLD 4538  domfiOLD 4539  isfinite2OLD 4546  unfilem1 4548  noinfep 4640  r1tr 4654  r1ord3 4657  bndrank 4682  aceq3 4733  fodom 4798  alephordi 4874  mulcanpi 5027  addnidpi 5028  ltexpq 5080  ltbtwnpq 5084  genpss 5107  genpcd 5109  genpnmax 5110  mulclprlem 5121  distrlem1pr 5127  distrlem4pr 5130  distrlem5pr 5131  ltexprlem3 5144  ltexprlem6 5147  ltexpri 5149  reclem4pr 5159  cnegextlem1 5345  lelttrt 5523  ltletrt 5524  letrt 5525  xrlelttrt 5562  xrltletrt 5563  xrletrt 5564  xrrebndt 5568  ltleaddt 5645  divadddivt 5784  lemul1it 5837  lemul1itOLD 5838  squeeze0 5924  avglet 6044  suprleub 6059  supxrleub 6099  elnnz 6145  elnnz1 6155  zltp1let 6181  zextltt 6190  uzind2 6206  uzindOLD 6208  qrecclt 6273  qbtwnre 6278  monoord 6294  om2uzf1o 6301  elioc2t 6390  elico2t 6391  elicc2t 6392  icoshft 6408  icoshftf1oi 6409  indstr 6461  elfzlem 6473  fsequb 6523  expwordit 6603  sqlecant 6641  sqr0 6672  sqrlem6 6678  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 7628  basgen2t 7639  bastop 7642  neips 7727  neindisj 7731  qdensere 7751  metxp 7834  bl2in 7843  rnblssm 7851  blss 7853  opnin 7869  metcnp 7887  blssioo 7913  tgioolem 7914  metelcls 7965  xplmi 7973  iscms2lem3 7991  lmcau 7996  cmsss 7997  bcthlem1 7999  bcthlem16 8014  bcthlem20 8018  bcthlem25 8023  ipasslem11 8500  psref 8649  pilem1 8671  sincosq3sgn 8706  sincosq4sgn 8707  efif1lem3 8732  efif1 8737  eff1i 8744  hlimunii 9108  chocuni 9172  projlem26 9211  h1de2ctlem 9478  spansneleq 9493  spansnsst 9494  normcant 9499  spansncv 9597  hmopidmchlem 10078  stadd3 10175  cvcon3t 10211  dmdbr5 10235  ssdmd2 10241  atom1d 10280  superpos 10281  cvexchlem 10295  atcv0eq 10306  atexcht 10308  atcvat4 10324  atdmd 10325  atmd2 10327  mdsymlem3 10332  mdsymlem5 10334  sumdmdlem 10345  cdjreu 10359  cdrci 10494  elioo1t3 10496  cnrsfin 10509  cnrscoa 10510  hmphsyma 10528  homcard 10539  set2elt 10545  iintlem1 10632  ismonb2 10740  icmpmon 10744  idmon 10745  isepib2 10750

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