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 1963  xp11 3483  foconst 3690  fvco 3781  isomin 3906  tfrlem5 3922  tz7.48lem 3962  oevn0 4161  oaass 4202  omword1 4211  omlimcl 4216  odi 4217  oneo 4219  oewordi 4225  oeworde 4227  th3qlem1 4321  dom2d 4411  fundmen 4435  unen 4441  onfin 4527  ssfi 4549  ssfiOLD 4550  domfi 4551  domfiOLD 4552  isfinite2 4559  isfinite2OLD 4560  unfilem1 4562  noinfep 4657  r1tr 4671  r1ord3 4674  bndrank 4699  aceq3 4750  fodom 4815  alephordi 4892  mulcanpi 5046  addnidpi 5047  ltexpq 5099  ltbtwnpq 5103  genpss 5126  genpcd 5128  genpnmax 5129  mulclprlem 5140  distrlem1pr 5146  distrlem4pr 5149  distrlem5pr 5150  ltexprlem3 5163  ltexprlem6 5166  ltexpri 5168  reclem4pr 5178  cnegextlem1 5364  lelttrt 5542  ltletrt 5543  letrt 5544  xrlelttrt 5581  xrltletrt 5582  xrletrt 5583  xrrebndt 5587  ltleaddt 5664  divadddivt 5793  lemul1it 5846  lemul1itOLD 5847  squeeze0 5933  avglet 6053  suprleub 6068  supxrleub 6108  elnnz 6154  elnnz1 6164  zltp1let 6190  zextltt 6199  uzind2 6215  uzindOLD 6217  qrecclt 6281  qbtwnre 6286  monoord 6302  om2uzf1o 6309  elioc2t 6398  elico2t 6399  elicc2t 6400  icoshft 6416  icoshftf1oi 6417  indstr 6469  elfzlem 6481  fsequb 6531  expwordit 6611  sqlecant 6649  sqr0 6680  sqrlem6 6686  absnidt 6870  seq1bnd 6917  cau3ir 6922  caubnd 6933  facdivt 6949  facwordit 6951  faclbnd 6952  bccl2t 6978  fsum1s 7016  clm4le 7088  climunii 7105  climshft 7111  climge0 7119  climsup 7162  climcau 7163  serzf0 7176  ser1f0 7177  expcnvlem6 7239  cvgratlem2 7258  ivthlem1 7288  reeff1 7417  reeff1o 7433  tgtopt 7634  basgen2t 7645  bastop 7648  neips 7731  neindisj 7735  qdensere 7755  metxp 7838  bl2in 7847  rnblssm 7855  blss 7857  opnin 7873  metcnp 7891  blssioo 7917  tgioolem 7918  metelcls 7969  xplmi 7977  iscms2lem3 7995  lmcau 8000  cmsss 8001  bcthlem1 8003  bcthlem16 8018  bcthlem20 8022  bcthlem25 8027  ipasslem11 8503  psref 8652  pilem1 8673  sincosq3sgn 8708  sincosq4sgn 8709  efif1lem3 8734  efif1 8739  eff1i 8746  hlimunii 9110  chocuni 9174  projlem26 9213  h1de2ctlem 9480  spansneleq 9495  spansnsst 9496  normcant 9501  spansncv 9599  hmopidmchlem 10080  stadd3 10178  cvcon3t 10214  dmdbr5 10238  ssdmd2 10244  atom1d 10283  superpos 10284  cvexchlem 10298  atcv0eq 10309  atexcht 10311  atcvat4 10327  atdmd 10328  atmd2 10330  mdsymlem3 10335  mdsymlem5 10337  sumdmdlem 10348  cdjreu 10362  cdrci 10488  elioo1t3 10490  cnrsfin 10503  cnrscoa 10504  hmphsyma 10522  homcard 10533  set2elt 10539  iintlem1 10611  ismonb2 10719  icmpmon 10723  idmon 10724  isepib2 10729

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