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 541  hbsb4 1243  ax11eq 1356  ax11el 1357  vtoclegft 1847  sbciegft 1949  xp11 3463  foconst 3668  fvco 3759  isomin 3884  tfrlem5 3900  tz7.48lem 3940  oevn0 4138  oaass 4179  omword1 4188  omlimcl 4193  odi 4194  oneo 4196  oewordi 4202  oeworde 4204  th3qlem1 4298  dom2d 4385  fundmen 4409  unen 4414  onfin 4499  ssfi 4515  domfi 4516  isfinite2 4523  unfilem1 4524  noinfep 4612  r1tr 4626  r1ord3 4629  bndrank 4654  aceq3 4705  fodom 4770  alephordi 4846  mulcanpi 4999  addnidpi 5000  ltexpq 5052  ltbtwnpq 5056  genpss 5079  genpcd 5081  genpnmax 5082  mulclprlem 5093  distrlem1pr 5099  distrlem4pr 5102  distrlem5pr 5103  ltexprlem3 5116  ltexprlem6 5119  ltexpri 5121  reclem4pr 5131  cnegextlem1 5317  lelttrt 5496  ltletrt 5497  letrt 5498  xrlelttrt 5535  xrltletrt 5536  xrletrt 5537  xrrebndt 5541  ltleaddt 5619  divadddivt 5740  lemul1it 5793  lemul1itOLD 5794  squeeze0 5872  avglet 5991  suprleub 6006  supxrleub 6046  elnnz 6092  elnnz1 6102  zltp1let 6128  zextltt 6137  uzind2 6154  uzindOLD 6156  qrecclt 6211  qbtwnre 6216  monoord 6231  om2uzf1o 6238  elioc2t 6322  elico2t 6323  elicc2t 6324  icoshft 6341  icoshftf1oi 6342  indstr 6393  elfzlem 6405  fsequb 6455  expwordit 6534  sqlecant 6572  sqr0 6602  sqrlem6 6608  absnidt 6798  seq1bnd 6847  cau3ir 6852  caubnd 6863  facdivt 6879  facwordit 6881  faclbnd 6882  bccl2t 6909  fsum1s 6947  clm4le 7019  climunii 7035  climshft 7041  climge0 7049  climsup 7091  climcau 7092  serzf0 7105  ser1f0 7106  expcnvlem6 7167  cvgratlem2 7186  ivthlem1 7216  reeff1 7350  reeff1o 7368  tgtopt 7570  basgen2t 7581  bastop 7584  neips 7668  neindisj 7672  qdensere 7691  metxp 7774  bl2in 7783  rnblssm 7791  blss 7793  opnin 7809  metcnp 7826  blssioo 7852  tgioolem 7853  metelcls 7900  xplmi 7907  iscms2lem3 7925  lmcau 7930  cmsss 7931  bcthlem1 7933  bcthlem16 7948  bcthlem20 7952  bcthlem25 7957  ipasslem11 8431  psref 8575  pilem1 8590  sincosq3sgn 8623  sincosq4sgn 8624  efif1lem3 8647  efif1 8652  eff1i 8665  hlimunii 9029  chocuni 9088  projlem26 9127  h1de2ctlem 9394  spansneleq 9409  spansneleqOLD 9410  spansnsst 9411  normcant 9416  spansncv 9514  hmopidmchlem 9989  stadd3 10085  cvcon3t 10121  ssdmd2 10149  atom1d 10188  superpos 10189  cvexchlem 10203  atcv0eq 10214  atexcht 10216  atcvat4 10232  atdmd 10233  atmd2 10235  mdsymlem3 10240  mdsymlem5 10242  sumdmdlem 10252  cdjreu 10264  cdrci 10381  elioo1t3 10383  cnrsfin 10396  cnrscoa 10397  hmphsyma 10415  homcard 10426  iintlem1 10476  ismonb2 10582  icmpmon 10587  idmon 10588

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