Theorem sylibd 241

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 231	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3imtr3d  295  csbiebt  3881  rspcsbela  4391  sneqrg  4796  preq1b  4803  csbexg  5259  elrnrexdm  7066  isoselem  7321  funeldmb  7339  riotass2  7379  ordzsl  7821  resf1extb  7911  oaword2  8517  oaordex  8522  omword1  8537  om00  8539  omeulem2  8547  oen0  8551  oeeui  8567  nnaordex  8603  php3  9173  frfi  9225  infglb  9434  suc11reg  9571  cardne  9920  cardsdomel  9929  carduni  9936  acndom  10004  alephinit  10048  cfflb  10213  cfslb2n  10222  fin23lem28  10294  isf34lem6  10334  fin1a2lem9  10362  axcc3  10392  winalim2  10651  inar1  10730  rankcf  10732  addclprlem2  10972  mulclprlem  10974  ltexprlem7  10997  prlem936  11002  reclem4pr  11005  sqgt0sr  11061  ltord2  11713  leord2  11714  eqord2  11715  mulgt1OLD  12047  mulge0b  12059  lt2halves  12453  addltmul  12454  ltsubnn0  12529  nzadd  12616  zextlt  12644  recnz  12645  zeo  12656  peano5uzi  12659  uzm1  12870  irradd  12971  irrmul  12972  xltneg  13217  xleadd1  13255  xmulasslem  13285  xlemul1a  13288  xlemul1  13290  fznuz  13611  uznfz  13612  axdc4uzlem  13993  facndiv  14298  hashvnfin  14370  hashgt12el  14432  hashgt12el2  14433  hashf1  14467  ccatalpha  14604  swrdccatin2  14739  swrdccatin2d  14754  rennim  15249  cau3lem  15365  caubnd2  15368  o1lo1  15547  climrlim2  15557  climshft  15586  subcn2  15605  mulcn2  15606  rlimo1  15627  o1dif  15640  isercoll  15678  caucvgrlem  15683  serf0  15691  cvgrat  15896  efieq1re  16214  moddvds  16280  dvdsssfz1  16335  smuval2  16499  nn0seqcvgd  16587  algcvgblem  16594  eucalglt  16602  lcmgcdlem  16623  rpmul  16676  divgcdcoprm0  16682  isprm6  16732  rpexp  16740  eulerthlem2  16800  prmdiv  16803  pcprendvds2  16860  pcz  16900  pcprmpw  16902  pcadd2  16909  pcfac  16918  expnprm  16921  ramlb  17038  firest  17444  joineu  18395  meeteu  18409  latjlej1  18468  latjlej2  18469  latmlem1  18484  latmlem2  18485  lubun  18530  acsmapd  18569  imasgrp2  19080  issubg4  19170  psgnunilem4  19520  oddvdsnn0  19567  odmulgeq  19580  subgpgp  19620  odcau  19627  lsmlub  19687  frgpnabllem1  19896  pgpfac1lem2  20100  pgpfac1lem3a  20101  pgpfac1lem3  20102  irredrmul  20455  isdomn4  20745  islmhm2  21085  lsmelval2  21132  lspsnat  21195  znidomb  21593  ip2eq  21685  lsmcss  21724  cnpnei  23304  cncls2  23313  cncls  23314  cnntr  23315  cnt0  23386  isnrm2  23398  comppfsc  23572  kqcldsat  23773  isr0  23777  hmeoopn  23806  hmeocld  23807  trufil  23950  opnsubg  24148  ghmcnp  24155  tgphaus  24157  qustgpopn  24160  tsmsgsum  24179  isngp4  24652  xrhmeo  24988  bndth  25000  cfilres  25338  caubl  25350  ivthlem2  25494  ovolicc2  25564  ismbf3d  25696  itg1ge0a  25753  mbfi1flim  25765  itg2gt0  25802  dvge0  26048  dvcnvrelem1  26059  dvcvx  26062  mdegmullem  26118  ig1peu  26215  plyco  26281  coemulc  26295  dgreq0  26305  dgrlt  26306  plymul0or  26322  plydiveu  26339  quotcan  26350  aalioulem3  26375  ulmcaulem  26434  sincosq3sgn  26542  sincosq4sgn  26543  sineq0  26566  logrec  26805  xrlimcnp  27010  cxploglim  27019  lgamgulmlem1  27070  mumul  27222  chtub  27253  perfect1  27269  dchrelbas3  27279  lgsdir2lem4  27369  lgsne0  27376  lgsquad2lem2  27426  2sqlem8a  27466  2sqblem  27472  nogt01o  27737  ltslpss  27978  ltadds2im  28056  ltnegs  28115  z12bday  28555  axcontlem2  29112  elntg2  29132  redwlklem  29816  redwlk  29817  crctcshwlkn0lem3  29958  crctcshwlkn0lem5  29960  clwwlkext2edg  30204  wwlksubclwwlk  30206  frgrwopregasn  30464  frgrwopregbsn  30465  blocnilem  30953  ip2eqi  31005  ubthlem2  31020  hial0  31251  hial02  31252  hial2eq  31255  h1datomi  31730  sumspansn  31798  lnopcnbd  32185  riesz4i  32212  bra11  32257  pjss2coi  32313  pjnormssi  32317  pjorthcoi  32318  pjclem4a  32347  pj3lem1  32355  pj3cor1i  32358  hst1h  32376  stm1i  32392  strlem1  32399  golem2  32421  mdbr2  32445  dmdbr5  32457  mdsl2i  32471  atexch  32530  atcvatlem  32534  chirredlem1  32539  cdjreui  32581  cdj1i  32582  cdj3lem1  32583  xraddge02  32909  submarchi  33327  isarchiofld  33340  esumcvg  34344  bnj1468  35105  loop1cycl  35451  erdsze2lem2  35518  btwnexch  36339  btwncolinear2  36384  btwncolinear3  36385  btwncolinear4  36386  btwncolinear5  36387  btwncolinear6  36388  nn0prpw  36647  cldbnd  36650  onsuct0  36765  onint1  36773  bj-ceqsalt0  37333  bj-ceqsalt1  37334  bj-inftyexpiinj  37665  bj-bary1lem1  37767  bj-bary1  37768  relowlssretop  37821  isinf2  37863  ltflcei  38071  tan2h  38075  poimirlem26  38109  poimirlem31  38114  ftc1anclem6  38161  dvasin  38167  dvacos  38168  fdc  38208  caushft  38224  heibor1lem  38272  bfplem2  38286  rrncmslem  38295  rngosn3  38387  mpobi123f  38625  riotasv3d  39548  lsatcv1  39636  lub0N  39777  glb0N  39781  oplecon3b  39788  cmtbr4N  39843  cvrnbtwn2  39863  atnlt  39901  atlatle  39908  cvlsupr2  39931  cvrexchlem  40007  cvratlem  40009  atcvrj0  40016  cvrat4  40031  cvrat42  40032  4noncolr3  40041  ps-1  40065  llnnlt  40111  lplnnlt  40153  lvolnltN  40206  dalempnes  40239  dalemqnet  40240  dalem-cly  40259  dalem44  40304  pmaple  40349  cdlemblem  40381  paddss  40433  2polcon4bN  40506  ltrneq2  40736  cdlemc3  40781  cdleme11h  40854  cdleme16b  40867  cdlemednpq  40887  tendospcanN  41611  dihmeetlem13N  41907  mapdordlem2  42225  mapdn0  42257  rspcsbnea  42712  ccatcan2d  42831  ctbnfien  43359  rmxypairf1o  43452  monotoddzzfi  43483  oddcomabszz  43485  acongtr  43519  onsupnmax  43769  onsupsucismax  43820  frege124d  44301  expgrowth  44875  sbcbi  45079  limsupmnflem  46258  funressnfv  47601  funfocofob  47636  2elfz2melfz  47876  iccpartnel  48008  requad2  48209  grlictr  48601  gpg5nbgrvtx13starlem1  48657  gpg5nbgrvtx13starlem3  48659  uzlidlring  48821  ply1mulgsumlem2  48973  fllog2  49154  dignn0flhalflem1  49201