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  3866  rspcsbela  4378  sneqrg  4782  preq1b  4789  csbexg  5245  elrnrexdm  7041  isoselem  7296  funeldmb  7314  riotass2  7354  ordzsl  7796  resf1extb  7885  oaword2  8488  oaordex  8493  omword1  8508  om00  8510  omeulem2  8518  oen0  8522  oeeui  8538  nnaordex  8574  php3  9143  frfi  9195  infglb  9404  suc11reg  9540  cardne  9889  cardsdomel  9898  carduni  9905  acndom  9973  alephinit  10017  cfflb  10181  cfslb2n  10190  fin23lem28  10262  isf34lem6  10302  fin1a2lem9  10330  axcc3  10360  winalim2  10619  inar1  10698  rankcf  10700  addclprlem2  10940  mulclprlem  10942  ltexprlem7  10965  prlem936  10970  reclem4pr  10973  sqgt0sr  11029  ltord2  11679  leord2  11680  eqord2  11681  mulgt1OLD  12014  mulge0b  12026  lt2halves  12412  addltmul  12413  ltsubnn0  12488  nzadd  12575  zextlt  12603  recnz  12604  zeo  12615  peano5uzi  12618  uzm1  12822  irradd  12923  irrmul  12924  xltneg  13169  xleadd1  13207  xmulasslem  13237  xlemul1a  13240  xlemul1  13242  fznuz  13563  uznfz  13564  axdc4uzlem  13945  facndiv  14250  hashvnfin  14322  hashgt12el  14384  hashgt12el2  14385  hashf1  14419  ccatalpha  14556  swrdccatin2  14691  swrdccatin2d  14706  rennim  15201  cau3lem  15317  caubnd2  15320  o1lo1  15499  climrlim2  15509  climshft  15538  subcn2  15557  mulcn2  15558  rlimo1  15579  o1dif  15592  isercoll  15630  caucvgrlem  15635  serf0  15643  cvgrat  15848  efieq1re  16166  moddvds  16232  dvdsssfz1  16287  smuval2  16451  nn0seqcvgd  16539  algcvgblem  16546  eucalglt  16554  lcmgcdlem  16575  rpmul  16628  divgcdcoprm0  16634  isprm6  16684  rpexp  16692  eulerthlem2  16752  prmdiv  16755  pcprendvds2  16812  pcz  16852  pcprmpw  16854  pcadd2  16861  pcfac  16870  expnprm  16873  ramlb  16990  firest  17395  joineu  18346  meeteu  18360  latjlej1  18419  latjlej2  18420  latmlem1  18435  latmlem2  18436  lubun  18481  acsmapd  18520  imasgrp2  19031  issubg4  19121  psgnunilem4  19472  oddvdsnn0  19519  odmulgeq  19532  subgpgp  19572  odcau  19579  lsmlub  19639  frgpnabllem1  19848  pgpfac1lem2  20052  pgpfac1lem3a  20053  pgpfac1lem3  20054  irredrmul  20407  isdomn4  20693  islmhm2  21033  lsmelval2  21080  lspsnat  21143  znidomb  21541  ip2eq  21633  lsmcss  21672  cnpnei  23229  cncls2  23238  cncls  23239  cnntr  23240  cnt0  23311  isnrm2  23323  comppfsc  23497  kqcldsat  23698  isr0  23702  hmeoopn  23731  hmeocld  23732  trufil  23875  opnsubg  24073  ghmcnp  24080  tgphaus  24082  qustgpopn  24085  tsmsgsum  24104  isngp4  24577  xrhmeo  24913  bndth  24925  cfilres  25263  caubl  25275  ivthlem2  25419  ovolicc2  25489  ismbf3d  25621  itg1ge0a  25678  mbfi1flim  25690  itg2gt0  25727  dvge0  25973  dvcnvrelem1  25984  dvcvx  25987  mdegmullem  26043  ig1peu  26140  plyco  26206  coemulc  26220  dgreq0  26230  dgrlt  26231  plymul0or  26247  plydiveu  26264  quotcan  26275  aalioulem3  26300  ulmcaulem  26359  sincosq3sgn  26464  sincosq4sgn  26465  sineq0  26488  logrec  26727  xrlimcnp  26932  cxploglim  26941  lgamgulmlem1  26992  mumul  27144  chtub  27175  perfect1  27191  dchrelbas3  27201  lgsdir2lem4  27291  lgsne0  27298  lgsquad2lem2  27348  2sqlem8a  27388  2sqblem  27394  nogt01o  27660  ltslpss  27900  ltadds2im  27978  ltnegs  28037  z12bday  28477  axcontlem2  29034  elntg2  29054  redwlklem  29738  redwlk  29739  crctcshwlkn0lem3  29880  crctcshwlkn0lem5  29882  clwwlkext2edg  30126  wwlksubclwwlk  30128  frgrwopregasn  30386  frgrwopregbsn  30387  blocnilem  30875  ip2eqi  30927  ubthlem2  30942  hial0  31173  hial02  31174  hial2eq  31177  h1datomi  31652  sumspansn  31720  lnopcnbd  32107  riesz4i  32134  bra11  32179  pjss2coi  32235  pjnormssi  32239  pjorthcoi  32240  pjclem4a  32269  pj3lem1  32277  pj3cor1i  32280  hst1h  32298  stm1i  32314  strlem1  32321  golem2  32343  mdbr2  32367  dmdbr5  32379  mdsl2i  32393  atexch  32452  atcvatlem  32456  chirredlem1  32461  cdjreui  32503  cdj1i  32504  cdj3lem1  32505  xraddge02  32830  submarchi  33247  isarchiofld  33260  esumcvg  34230  bnj1468  34988  loop1cycl  35319  erdsze2lem2  35386  btwnexch  36207  btwncolinear2  36252  btwncolinear3  36253  btwncolinear4  36254  btwncolinear5  36255  btwncolinear6  36256  nn0prpw  36505  cldbnd  36508  onsuct0  36623  onint1  36631  bj-ceqsalt0  37191  bj-ceqsalt1  37192  bj-inftyexpiinj  37523  bj-bary1lem1  37625  bj-bary1  37626  relowlssretop  37679  isinf2  37721  ltflcei  37929  tan2h  37933  poimirlem26  37967  poimirlem31  37972  ftc1anclem6  38019  dvasin  38025  dvacos  38026  fdc  38066  caushft  38082  heibor1lem  38130  bfplem2  38144  rrncmslem  38153  rngosn3  38245  mpobi123f  38483  riotasv3d  39406  lsatcv1  39494  lub0N  39635  glb0N  39639  oplecon3b  39646  cmtbr4N  39701  cvrnbtwn2  39721  atnlt  39759  atlatle  39766  cvlsupr2  39789  cvrexchlem  39865  cvratlem  39867  atcvrj0  39874  cvrat4  39889  cvrat42  39890  4noncolr3  39899  ps-1  39923  llnnlt  39969  lplnnlt  40011  lvolnltN  40064  dalempnes  40097  dalemqnet  40098  dalem-cly  40117  dalem44  40162  pmaple  40207  cdlemblem  40239  paddss  40291  2polcon4bN  40364  ltrneq2  40594  cdlemc3  40639  cdleme11h  40712  cdleme16b  40725  cdlemednpq  40745  tendospcanN  41469  dihmeetlem13N  41765  mapdordlem2  42083  mapdn0  42115  rspcsbnea  42570  ccatcan2d  42690  ctbnfien  43246  rmxypairf1o  43339  monotoddzzfi  43370  oddcomabszz  43372  acongtr  43406  onsupnmax  43656  onsupsucismax  43707  frege124d  44188  expgrowth  44762  sbcbi  44966  limsupmnflem  46148  funressnfv  47491  funfocofob  47526  2elfz2melfz  47766  iccpartnel  47898  requad2  48099  grlictr  48491  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem3  48549  uzlidlring  48711  ply1mulgsumlem2  48863  fllog2  49044  dignn0flhalflem1  49091