Theorem sylibd 239

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

Hypotheses

Ref	Expression
sylibd.1	⊢ (𝜑 → (𝜓 → 𝜒))
sylibd.2	⊢ (𝜑 → (𝜒 ↔ 𝜃))

Assertion

Ref	Expression
sylibd	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylibd

Step	Hyp	Ref	Expression
1		sylibd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylibd.2	. . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃))
3	2	biimpd 229	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3imtr3d  293  csbiebt  3878  rspcsbela  4390  sneqrg  4795  preq1b  4802  csbexg  5255  elrnrexdm  7034  isoselem  7287  funeldmb  7305  riotass2  7345  ordzsl  7787  resf1extb  7876  oaword2  8480  oaordex  8485  omword1  8500  om00  8502  omeulem2  8510  oen0  8514  oeeui  8530  nnaordex  8566  php3  9133  frfi  9185  infglb  9394  suc11reg  9528  cardne  9877  cardsdomel  9886  carduni  9893  acndom  9961  alephinit  10005  cfflb  10169  cfslb2n  10178  fin23lem28  10250  isf34lem6  10290  fin1a2lem9  10318  axcc3  10348  winalim2  10607  inar1  10686  rankcf  10688  addclprlem2  10928  mulclprlem  10930  ltexprlem7  10953  prlem936  10958  reclem4pr  10961  sqgt0sr  11017  ltord2  11666  leord2  11667  eqord2  11668  mulgt1OLD  12000  mulge0b  12012  lt2halves  12376  addltmul  12377  ltsubnn0  12452  nzadd  12539  zextlt  12566  recnz  12567  zeo  12578  peano5uzi  12581  uzm1  12785  irradd  12886  irrmul  12887  xltneg  13132  xleadd1  13170  xmulasslem  13200  xlemul1a  13203  xlemul1  13205  fznuz  13525  uznfz  13526  axdc4uzlem  13906  facndiv  14211  hashvnfin  14283  hashgt12el  14345  hashgt12el2  14346  hashf1  14380  ccatalpha  14517  swrdccatin2  14652  swrdccatin2d  14667  rennim  15162  cau3lem  15278  caubnd2  15281  o1lo1  15460  climrlim2  15470  climshft  15499  subcn2  15518  mulcn2  15519  rlimo1  15540  o1dif  15553  isercoll  15591  caucvgrlem  15596  serf0  15604  cvgrat  15806  efieq1re  16124  moddvds  16190  dvdsssfz1  16245  smuval2  16409  nn0seqcvgd  16497  algcvgblem  16504  eucalglt  16512  lcmgcdlem  16533  rpmul  16586  divgcdcoprm0  16592  isprm6  16641  rpexp  16649  eulerthlem2  16709  prmdiv  16712  pcprendvds2  16769  pcz  16809  pcprmpw  16811  pcadd2  16818  pcfac  16827  expnprm  16830  ramlb  16947  firest  17352  joineu  18303  meeteu  18317  latjlej1  18376  latjlej2  18377  latmlem1  18392  latmlem2  18393  lubun  18438  acsmapd  18477  imasgrp2  18985  issubg4  19075  psgnunilem4  19426  oddvdsnn0  19473  odmulgeq  19486  subgpgp  19526  odcau  19533  lsmlub  19593  frgpnabllem1  19802  pgpfac1lem2  20006  pgpfac1lem3a  20007  pgpfac1lem3  20008  irredrmul  20363  isdomn4  20649  islmhm2  20990  lsmelval2  21037  lspsnat  21100  znidomb  21516  ip2eq  21608  lsmcss  21647  cnpnei  23208  cncls2  23217  cncls  23218  cnntr  23219  cnt0  23290  isnrm2  23302  comppfsc  23476  kqcldsat  23677  isr0  23681  hmeoopn  23710  hmeocld  23711  trufil  23854  opnsubg  24052  ghmcnp  24059  tgphaus  24061  qustgpopn  24064  tsmsgsum  24083  isngp4  24556  xrhmeo  24900  bndth  24913  cfilres  25252  caubl  25264  ivthlem2  25409  ovolicc2  25479  ismbf3d  25611  itg1ge0a  25668  mbfi1flim  25680  itg2gt0  25717  dvge0  25967  dvcnvrelem1  25978  dvcvx  25981  mdegmullem  26039  ig1peu  26136  plyco  26202  coemulc  26216  dgreq0  26227  dgrlt  26228  plymul0or  26244  plydiveu  26262  quotcan  26273  aalioulem3  26298  ulmcaulem  26359  sincosq3sgn  26465  sincosq4sgn  26466  sineq0  26489  logrec  26729  xrlimcnp  26934  cxploglim  26944  lgamgulmlem1  26995  mumul  27147  chtub  27179  perfect1  27195  dchrelbas3  27205  lgsdir2lem4  27295  lgsne0  27302  lgsquad2lem2  27352  2sqlem8a  27392  2sqblem  27398  nogt01o  27664  ltslpss  27904  ltadds2im  27982  ltnegs  28041  z12bday  28481  axcontlem2  29038  elntg2  29058  redwlklem  29743  redwlk  29744  crctcshwlkn0lem3  29885  crctcshwlkn0lem5  29887  clwwlkext2edg  30131  wwlksubclwwlk  30133  frgrwopregasn  30391  frgrwopregbsn  30392  blocnilem  30879  ip2eqi  30931  ubthlem2  30946  hial0  31177  hial02  31178  hial2eq  31181  h1datomi  31656  sumspansn  31724  lnopcnbd  32111  riesz4i  32138  bra11  32183  pjss2coi  32239  pjnormssi  32243  pjorthcoi  32244  pjclem4a  32273  pj3lem1  32281  pj3cor1i  32284  hst1h  32302  stm1i  32318  strlem1  32325  golem2  32347  mdbr2  32371  dmdbr5  32383  mdsl2i  32397  atexch  32456  atcvatlem  32460  chirredlem1  32465  cdjreui  32507  cdj1i  32508  cdj3lem1  32509  xraddge02  32837  submarchi  33268  isarchiofld  33281  esumcvg  34243  bnj1468  35002  loop1cycl  35331  erdsze2lem2  35398  btwnexch  36219  btwncolinear2  36264  btwncolinear3  36265  btwncolinear4  36266  btwncolinear5  36267  btwncolinear6  36268  nn0prpw  36517  cldbnd  36520  onsuct0  36635  onint1  36643  bj-ceqsalt0  37085  bj-ceqsalt1  37086  bj-inftyexpiinj  37410  bj-bary1lem1  37512  bj-bary1  37513  relowlssretop  37564  isinf2  37606  ltflcei  37805  tan2h  37809  poimirlem26  37843  poimirlem31  37848  ftc1anclem6  37895  dvasin  37901  dvacos  37902  fdc  37942  caushft  37958  heibor1lem  38006  bfplem2  38020  rrncmslem  38029  rngosn3  38121  mpobi123f  38359  riotasv3d  39216  lsatcv1  39304  lub0N  39445  glb0N  39449  oplecon3b  39456  cmtbr4N  39511  cvrnbtwn2  39531  atnlt  39569  atlatle  39576  cvlsupr2  39599  cvrexchlem  39675  cvratlem  39677  atcvrj0  39684  cvrat4  39699  cvrat42  39700  4noncolr3  39709  ps-1  39733  llnnlt  39779  lplnnlt  39821  lvolnltN  39874  dalempnes  39907  dalemqnet  39908  dalem-cly  39927  dalem44  39972  pmaple  40017  cdlemblem  40049  paddss  40101  2polcon4bN  40174  ltrneq2  40404  cdlemc3  40449  cdleme11h  40522  cdleme16b  40535  cdlemednpq  40555  tendospcanN  41279  dihmeetlem13N  41575  mapdordlem2  41893  mapdn0  41925  rspcsbnea  42381  ccatcan2d  42502  ctbnfien  43056  rmxypairf1o  43149  monotoddzzfi  43180  oddcomabszz  43182  acongtr  43216  onsupnmax  43466  onsupsucismax  43517  frege124d  43998  expgrowth  44572  sbcbi  44776  limsupmnflem  45960  funressnfv  47285  funfocofob  47320  2elfz2melfz  47560  iccpartnel  47680  requad2  47865  grlictr  48257  gpg5nbgrvtx13starlem1  48313  gpg5nbgrvtx13starlem3  48315  uzlidlring  48477  ply1mulgsumlem2  48629  fllog2  48810  dignn0flhalflem1  48857