Theorem sylibd 218

Description: A syllogism deduction.

Hypotheses

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

Assertion

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

Proof of Theorem sylibd

Step	Hyp	Ref	Expression
1		sylibd.1	. 2 |- (ph -> (ps -> ch))
2		sylibd.2	. . 3 |- (ph -> (ch <-> th))
3	2	biimpd 169	. 2 |- (ph -> (ch -> th))
4	1, 3	syld 30	1 |- (ph -> (ps -> th))

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

This theorem is referenced by:  bitrd 584  3imtr3d 598  euimOLD 1655  sbceqal 2335  sbcbid 2337  eqsbc3r 2340  sbcimdv 2352  ra4esbca 2371  csbeq2d 2394  ra4csbela 2420  copsexg 3352  reuuniss2 3628  ordzsl 3738  fvopab2 4565  reiotass2 4922  oaword2 5046  oaordex 5051  omword1 5063  om00 5065  oen0 5072  oeordi 5073  php3 5419  onomeneq 5422  fodomfib 5467  suc11reg 5520  rankr1 5594  infenomsub 5685  aceq3lem 5690  ac6lem 5712  cardne 5776  cardaleph 5829  ltexpq 6028  addclprlem1 6066  addclprlem2 6067  mulclprlem 6069  ltexprlem7 6096  prlem936b 6102  reclem4pr 6107  sqgt0sr 6163  cnegexlem1 6295  addcaniOLD 6302  mulcani 6674  mulgt1 6822  nnleltp1 6933  lt2halves 7023  addltmul 7024  zextlt 7197  recnz 7198  zeo 7206  uzindOLD 7215  irradd 7252  irrmul 7253  qbtwnre 7254  flwordi 7272  expnlbnd2 7698  sqr2irr 7774  facndiv 7990  fsum1s 8064  2climnn 8157  2climnn0 8158  climge0 8167  climaddlem3 8171  caucvglem5 8216  caucvglem6 8217  caucvgi 8218  serzf0i 8224  cvgratlem1ALT 8304  cvgratlem1 8307  cvgratlem2 8308  efieq1re 8546  cnpnei 8838  dnsconst 8860  lmnn 9008  lmuni 9024  lmle 9033  metelcls 9038  metcnp4 9043  cmsss 9070  vacnlem3 9464  blocnilem 9599  ip2eqi 9653  minveclem27 9711  minveceu 9723  sincosq3sgn 9850  sincosq4sgn 9851  sineq0re 9862  eff1i 9893  uptx 10018  txcn 10019  fbunfip 10074  hial0 10393  hial02 10394  hial2eq 10397  chocunii 10597  shlej1 10780  h1datomi 10929  sumspansn 11021  lnopcnbd 11394  riesz4i 11425  bra11 11471  pjss2coi 11528  pjnormssi 11532  pjorthcoi 11533  pjclem4a 11563  pj3lem1 11571  pj3cor1i 11574  hst1h 11591  stm1i 11607  strlem1 11614  golem2 11636  mdbr2 11660  dmdbr5 11672  mdsl2i 11686  atexch 11745  atcvatlem 11749  irredlem1 11754  cdjreui 11796  cdj1i 11797  cdj3lem1 11798  bnj1468 12937  ghomf1olem 13429  nn0seqcvgd 13451  dvdsadd 13480  algcvgblem 13537  coprmdvds 13575  fprod1s 14401  trooo 14481  cntrsetlem 14709  idmon 14848  ioodisj 15046  elfiun 15051  infenomsubOLD 15080  cldbnd 15092  cnsubsp2 15109  reconnlem1 15128  locfincf 15198  comppfsc 15199  ufileu 15255  fmfnfmlem2 15277  fcluscnp 15300  ufcomp 15304  uzm1 15466  fdc 15494  mettrifi2 15530  caushft 15533  hmeoopn 15581  totbndss 15619  heiborlem15 15651  heiborlem16 15652  pcoass 15767  smoge 16136  latjlej1 16624  latjlej2 16625  latmlem1 16634  latmlem2 16635  glb0 16675  oplecon3b 16681  cmtbr4 16726  cvrnbtwn2 16742  hlatle 16791  cvrexchlem 16797  cvratlem 16799  atcvr1 16803  cvrat4 16806  ps-1 16807  pmaple 16967

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 163

Copyright terms: Public domain