Theorem sylibd 229

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

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 219	. 2 |- ( ph -> ( ch -> th ) )
4	1, 3	syld 47	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   <-> wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  3imtr3d  282  ceqsalt  3228  sbceqal  3487  csbiebt  3553  rspcsbela  4006  sneqrg  4370  preq1b  4377  csbexg  4792  elrnrexdm  6363  isoselem  6591  riotass2  6638  ordzsl  7045  oaword2  7633  oaordex  7638  omword1  7653  om00  7655  omeulem2  7663  oen0  7666  oeeui  7682  nnaordex  7718  php3  8146  onomeneq  8150  frfi  8205  infglb  8396  suc11reg  8516  cardne  8791  cardsdomel  8800  carduni  8807  acndom  8874  alephinit  8918  cfflb  9081  cfslb2n  9090  fin23lem28  9162  isf34lem6  9202  fin1a2lem9  9230  axcc3  9260  winalim2  9518  inar1  9597  rankcf  9599  addclprlem2  9839  mulclprlem  9841  ltexprlem7  9864  prlem936  9869  reclem4pr  9872  sqgt0sr  9927  ltord2  10557  leord2  10558  eqord2  10559  mulgt1  10882  mulge0b  10893  fiminre  10972  lt2halves  11267  addltmul  11268  ltsubnn0  11344  nzadd  11425  zextlt  11451  recnz  11452  zeo  11463  peano5uzi  11466  uzm1  11718  irradd  11812  irrmul  11813  xltneg  12048  xleadd1  12085  xmulasslem  12115  xlemul1a  12118  xlemul1  12120  fznuz  12422  uznfz  12423  axdc4uzlem  12782  facndiv  13075  hashvnfin  13151  hashgt12el  13210  hashgt12el2  13211  hashf1  13241  ccatalpha  13375  swrdccatin2  13487  swrdccatin2d  13500  swrdccatin12d  13501  rennim  13979  cau3lem  14094  caubnd2  14097  o1lo1  14268  climrlim2  14278  climshft  14307  subcn2  14325  mulcn2  14326  rlimo1  14347  o1dif  14360  isercoll  14398  caucvgrlem  14403  serf0  14411  cvgrat  14615  efieq1re  14929  moddvds  14991  dvdsssfz1  15040  smuval2  15204  nn0seqcvgd  15283  algcvgblem  15290  eucalglt  15298  lcmgcdlem  15319  coprmdvdsOLD  15367  rpmul  15373  divgcdcoprm0  15379  isprm6  15426  rpexp  15432  eulerthlem2  15487  prmdiv  15490  pcprendvds2  15546  pcz  15585  pcprmpw  15587  pcadd2  15594  pcfac  15603  expnprm  15606  ramlb  15723  firest  16093  joineu  17010  meeteu  17024  latjlej1  17065  latjlej2  17066  latmlem1  17081  latmlem2  17082  lubun  17123  acsmapd  17178  imasgrp2  17530  issubg4  17613  psgnunilem4  17917  oddvdsnn0  17963  odmulgeq  17974  subgpgp  18012  odcau  18019  lsmlub  18078  frgpnabllem1  18276  pgpfac1lem2  18474  pgpfac1lem3a  18475  pgpfac1lem3  18476  irredrmul  18707  islmhm2  19038  lsmelval2  19085  lspsnat  19145  znidomb  19910  ip2eq  19998  lsmcss  20036  cnpnei  21068  cncls2  21077  cncls  21078  cnntr  21079  cnt0  21150  isnrm2  21162  comppfsc  21335  kqcldsat  21536  isr0  21540  hmeoopn  21569  hmeocld  21570  trufil  21714  opnsubg  21911  ghmcnp  21918  tgphaus  21920  qustgpopn  21923  tsmsgsum  21942  isngp4  22416  xrhmeo  22745  bndth  22757  cfilres  23094  caubl  23106  ivthlem2  23221  ovolicc2  23290  ismbf3d  23421  itg1ge0a  23478  mbfi1flim  23490  itg2gt0  23527  dvge0  23769  dvcnvrelem1  23780  dvcvx  23783  mdegmullem  23838  ig1peu  23931  plyco  23997  coemulc  24011  dgreq0  24021  dgrlt  24022  plymul0or  24036  plydiveu  24053  quotcan  24064  aalioulem3  24089  ulmcaulem  24148  sincosq3sgn  24252  sincosq4sgn  24253  sineq0  24273  logrec  24501  xrlimcnp  24695  cxploglim  24704  lgamgulmlem1  24755  mumul  24907  chtub  24937  perfect1  24953  dchrelbas3  24963  lgsdir2lem4  25053  lgsne0  25060  lgsquad2lem2  25110  2sqlem8a  25150  2sqblem  25156  axcontlem2  25845  redwlklem  26568  redwlk  26569  crctcshwlkn0lem3  26704  crctcshwlkn0lem5  26706  clwwlksext2edg  26923  wwlksubclwwlks  26925  clwlksf1clwwlklem  26968  frgrwopregasn  27180  frgrwopregbsn  27181  blocnilem  27659  ip2eqi  27712  ubthlem2  27727  hial0  27959  hial02  27960  hial2eq  27963  h1datomi  28440  sumspansn  28508  lnopcnbd  28895  riesz4i  28922  bra11  28967  pjss2coi  29023  pjnormssi  29027  pjorthcoi  29028  pjclem4a  29057  pj3lem1  29065  pj3cor1i  29068  hst1h  29086  stm1i  29102  strlem1  29109  golem2  29131  mdbr2  29155  dmdbr5  29167  mdsl2i  29181  atexch  29240  atcvatlem  29244  chirredlem1  29249  cdjreui  29291  cdj1i  29292  cdj3lem1  29293  xraddge02  29521  submarchi  29740  isarchiofld  29817  esumcvg  30148  bnj1468  30916  erdsze2lem2  31186  funeldmb  31661  btwnexch  32132  btwncolinear2  32177  btwncolinear3  32178  btwncolinear4  32179  btwncolinear5  32180  btwncolinear6  32181  nn0prpw  32318  cldbnd  32321  onsuct0  32440  onint1  32448  bj-ceqsalt0  32873  bj-ceqsalt1  32874  bj-inftyexpiinj  33096  bj-bary1lem1  33161  bj-bary1  33162  relowlssretop  33211  ltflcei  33397  tan2h  33401  poimirlem26  33435  poimirlem31  33440  ftc1anclem6  33490  dvasin  33496  dvacos  33497  fdc  33541  caushft  33557  heibor1lem  33608  bfplem2  33622  rrncmslem  33631  rngosn3  33723  mpt2bi123f  33971  riotasv3d  34246  lsatcv1  34335  lub0N  34476  glb0N  34480  oplecon3b  34487  cmtbr4N  34542  cvrnbtwn2  34562  atnlt  34600  atlatle  34607  cvlsupr2  34630  cvrexchlem  34705  cvratlem  34707  atcvrj0  34714  cvrat4  34729  cvrat42  34730  4noncolr3  34739  ps-1  34763  llnnlt  34809  lplnnlt  34851  lvolnltN  34904  dalempnes  34937  dalemqnet  34938  dalem-cly  34957  dalem44  35002  pmaple  35047  cdlemblem  35079  paddss  35131  2polcon4bN  35204  ltrneq2  35434  cdlemc3  35480  cdleme11h  35553  cdleme16b  35566  cdlemednpq  35586  tendospcanN  36312  dihmeetlem13N  36608  mapdordlem2  36926  mapdn0  36958  ctbnfien  37382  rmxypairf1o  37476  monotoddzzfi  37507  oddcomabszz  37509  acongtr  37545  frege124d  38053  expgrowth  38534  sbcbi  38749  csbeq2gOLD  38765  limsupmnflem  39952  funressnfv  41208  2elfz2melfz  41328  iccpartnel  41374  uzlidlring  41929  ply1mulgsumlem2  42175  fllog2  42362  dignn0flhalflem1  42409