Theorem sylbid 201

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 151	. 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 144

This theorem is referenced by:  3imtr4d 546  hbsb4 1286  ax11eq 1402  ax11el 1403  vtoclegft 1902  sbciegft 2007  xp11 3561  foconst 3791  fvco 3885  isomin 4013  tfrlem5 4216  tz7.48lem 4256  oevn0 4290  oaass 4331  omword1 4340  omlimcl 4345  odi 4346  oneo 4348  oewordi 4354  oeworde 4356  th3qlem1 4455  dom2d 4545  fundmen 4569  unen 4575  ac6sfilem3 4590  onfin 4666  ssfi 4683  domfi 4684  isfinite2 4692  unfilem1 4694  noinfep 4786  r1tr 4800  r1ord3 4803  bndrank 4828  aceq3 4879  fodom 4944  alephordi 5024  mulcanpi 5181  addnidpi 5182  ltexpq 5234  ltbtwnpq 5238  genpss 5261  genpcd 5263  genpnmax 5264  mulclprlem 5275  distrlem1pr 5281  distrlem4pr 5284  distrlem5pr 5285  ltexprlem3 5298  ltexprlem6 5301  ltexpri 5303  reclem4pr 5313  cnegexlem1 5499  lelttr 5677  ltletr 5678  letr 5679  xrlelttr 5716  xrltletr 5717  xrletr 5718  xrrebnd 5722  ltleadd 5799  lemul1a 5981  lemul1aOLD 5982  squeeze0 6069  avgle 6190  suprleub 6227  supxrleub 6267  elnnz 6313  elnnz1 6323  zltp1le 6349  zextlt 6361  uzind2 6377  uzindOLD 6379  qreccl 6412  qbtwnre 6418  modirr 6481  monoord 6482  elioc2 6516  elico2 6517  elicc2 6518  icoshft 6535  icoshftf1oii 6536  indstr 6588  elfzlem 6601  fsequb 6654  om2uzf1oi 6664  expwordi 6800  sqlecan 6838  sqr0 6873  sqrlem6 6879  absnid 7065  seq1bndi 7113  cau3iri 7118  caubndi 7129  facdiv 7145  facwordi 7147  faclbnd 7148  bccl2 7174  fsum1s 7212  clm4lei 7284  climunii 7301  climshfti 7307  climge0 7315  climsupi 7358  climcaui 7359  serzf0i 7372  expcnvlem6 7436  cvgratlem2 7456  ivthlem1 7486  reeff1 7618  reeff1o 7634  efieq1re 7694  tgtop 7840  basgen2 7851  bastop1 7854  neips 7937  neindisj 7941  qdensere 7961  metxp 8044  bl2in 8053  rnblssm 8061  blss 8063  opnin 8079  metcnp 8098  blssioo 8124  tgioolem 8125  metelcls 8176  xplmi 8184  iscms2lem3 8202  lmcau 8207  cmsss 8208  bcthlem1 8210  bcthlem16 8225  bcthlem20 8229  bcthlem25 8234  vacnlem3 8584  ipasslem11 8756  psref 8911  pilem1 8938  sincosq3sgn 8973  sincosq4sgn 8974  sineq0re 8985  efif1lem3 9004  efif1 9009  eff1i 9016  hlimuniii 9384  chocunii 9448  projlem26 9487  h1de2ctlem 9754  spansneleq 9769  spansnss 9770  normcan 9775  spansncvi 9875  hmopidmchlem 10358  stadd3i 10456  cvcon3 10492  dmdbr5 10516  ssdmd2 10522  atom1d 10561  superpos 10562  cvexchlem 10576  atcv0eq 10588  atexch 10590  atcvat4i 10606  atdmd 10607  atmd2 10609  mdsymlem3 10614  mdsymlem5 10616  sumdmdlem 10627  cdjreui 10641  njtlc 10804  set2elt 10827  dupos1 10876  cdrci 10994  elioo1t3 10996  cnrsfin 11012  cnrscoa 11013  hmphsyma 11034  homcard 11045  bwt2 11123  altretop 11144  iintlem1 11155  ismonb2 11267  icmpmon 11271  idmon 11272  isepib2 11277  ccid 11412  fiuni 11420  elfiun 11421  ordiso 11426  ordtypelem6 11432  hartog 11436  omsubsdom 11442  omsubdom 11443  omsubel 11444  infenomsub 11450  cldbnd 11462  subsubtop 11479  subcld 11480  cnsubsp2 11484  compsublem 11487  compsub 11488  uncomp 11490  hscptsscld 11491  comptoppr 11495  alexsub 11500  connsub 11502  conntoppr 11504  reconnlem1 11507  2ndc1stc 11538  isfne3 11543  topfneec2 11563  comppfsc 11578  fnemeet1 11589  fnemeet2 11590  fgid 11637  fgmin 11639  ufileulem 11657  ufileu 11658  filufint 11659  ufinffr 11663  ufilen 11664  filcon 11665  flimopn 11679  cnpfillim 11686  elfilmap 11690  elfilmap2 11691  rnelfmlem 11698  rnelfm 11699  fmfnfmlem1 11700  fmfnfmlem2 11701  fmfnfmlem4 11703  flimfbas 11713  flimfnfcls 11727  uffclsflim 11728  fcluscomplem 11732  isfclusf 11737  tailmap 11759  tailfb 11762  filnetlem5 11767  filnet 11768  gapmlem 11783  indexd 11846  inficl 11849  fzm1 11867  incsequz 11879  fsum00 11883  subspcld2 11902  subspabs 11903  blhalf 11911  mettrifi2 11913  geomcau 11914  iccsplit 11919  iccss2 11921  cnimass 11949  cnresima 11952  cnss 11953  haustlmu 11967  lmtlm 11969  uptx 11978  txsubsp 11983  sstotbnd 11992  ismtybndlem 12008  heiborlem11 12021  heiborlem15 12025  recms 12066  rrnmet 12072  rrncms 12075  rrntotbnd 12078  iccbnd 12082

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 145

Copyright terms: Public domain