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  3875  rspcsbela  4387  sneqrg  4790  preq1b  4797  csbexg  5250  elrnrexdm  7028  isoselem  7281  funeldmb  7299  riotass2  7339  ordzsl  7781  resf1extb  7870  oaword2  8474  oaordex  8479  omword1  8494  om00  8496  omeulem2  8504  oen0  8507  oeeui  8523  nnaordex  8559  php3  9125  frfi  9176  infglb  9382  suc11reg  9516  cardne  9865  cardsdomel  9874  carduni  9881  acndom  9949  alephinit  9993  cfflb  10157  cfslb2n  10166  fin23lem28  10238  isf34lem6  10278  fin1a2lem9  10306  axcc3  10336  winalim2  10594  inar1  10673  rankcf  10675  addclprlem2  10915  mulclprlem  10917  ltexprlem7  10940  prlem936  10945  reclem4pr  10948  sqgt0sr  11004  ltord2  11653  leord2  11654  eqord2  11655  mulgt1OLD  11987  mulge0b  11999  lt2halves  12363  addltmul  12364  ltsubnn0  12439  nzadd  12526  zextlt  12553  recnz  12554  zeo  12565  peano5uzi  12568  uzm1  12772  irradd  12873  irrmul  12874  xltneg  13118  xleadd1  13156  xmulasslem  13186  xlemul1a  13189  xlemul1  13191  fznuz  13511  uznfz  13512  axdc4uzlem  13892  facndiv  14197  hashvnfin  14269  hashgt12el  14331  hashgt12el2  14332  hashf1  14366  ccatalpha  14503  swrdccatin2  14638  swrdccatin2d  14653  rennim  15148  cau3lem  15264  caubnd2  15267  o1lo1  15446  climrlim2  15456  climshft  15485  subcn2  15504  mulcn2  15505  rlimo1  15526  o1dif  15539  isercoll  15577  caucvgrlem  15582  serf0  15590  cvgrat  15792  efieq1re  16110  moddvds  16176  dvdsssfz1  16231  smuval2  16395  nn0seqcvgd  16483  algcvgblem  16490  eucalglt  16498  lcmgcdlem  16519  rpmul  16572  divgcdcoprm0  16578  isprm6  16627  rpexp  16635  eulerthlem2  16695  prmdiv  16698  pcprendvds2  16755  pcz  16795  pcprmpw  16797  pcadd2  16804  pcfac  16813  expnprm  16816  ramlb  16933  firest  17338  joineu  18288  meeteu  18302  latjlej1  18361  latjlej2  18362  latmlem1  18377  latmlem2  18378  lubun  18423  acsmapd  18462  imasgrp2  18970  issubg4  19060  psgnunilem4  19411  oddvdsnn0  19458  odmulgeq  19471  subgpgp  19511  odcau  19518  lsmlub  19578  frgpnabllem1  19787  pgpfac1lem2  19991  pgpfac1lem3a  19992  pgpfac1lem3  19993  irredrmul  20347  isdomn4  20633  islmhm2  20974  lsmelval2  21021  lspsnat  21084  znidomb  21500  ip2eq  21592  lsmcss  21631  cnpnei  23180  cncls2  23189  cncls  23190  cnntr  23191  cnt0  23262  isnrm2  23274  comppfsc  23448  kqcldsat  23649  isr0  23653  hmeoopn  23682  hmeocld  23683  trufil  23826  opnsubg  24024  ghmcnp  24031  tgphaus  24033  qustgpopn  24036  tsmsgsum  24055  isngp4  24528  xrhmeo  24872  bndth  24885  cfilres  25224  caubl  25236  ivthlem2  25381  ovolicc2  25451  ismbf3d  25583  itg1ge0a  25640  mbfi1flim  25652  itg2gt0  25689  dvge0  25939  dvcnvrelem1  25950  dvcvx  25953  mdegmullem  26011  ig1peu  26108  plyco  26174  coemulc  26188  dgreq0  26199  dgrlt  26200  plymul0or  26216  plydiveu  26234  quotcan  26245  aalioulem3  26270  ulmcaulem  26331  sincosq3sgn  26437  sincosq4sgn  26438  sineq0  26461  logrec  26701  xrlimcnp  26906  cxploglim  26916  lgamgulmlem1  26967  mumul  27119  chtub  27151  perfect1  27167  dchrelbas3  27177  lgsdir2lem4  27267  lgsne0  27274  lgsquad2lem2  27324  2sqlem8a  27364  2sqblem  27370  nogt01o  27636  sltlpss  27854  sltadd2im  27930  sltneg  27988  axcontlem2  28945  elntg2  28965  redwlklem  29650  redwlk  29651  crctcshwlkn0lem3  29792  crctcshwlkn0lem5  29794  clwwlkext2edg  30038  wwlksubclwwlk  30040  frgrwopregasn  30298  frgrwopregbsn  30299  blocnilem  30786  ip2eqi  30838  ubthlem2  30853  hial0  31084  hial02  31085  hial2eq  31088  h1datomi  31563  sumspansn  31631  lnopcnbd  32018  riesz4i  32045  bra11  32090  pjss2coi  32146  pjnormssi  32150  pjorthcoi  32151  pjclem4a  32180  pj3lem1  32188  pj3cor1i  32191  hst1h  32209  stm1i  32225  strlem1  32232  golem2  32254  mdbr2  32278  dmdbr5  32290  mdsl2i  32304  atexch  32363  atcvatlem  32367  chirredlem1  32372  cdjreui  32414  cdj1i  32415  cdj3lem1  32416  xraddge02  32744  submarchi  33162  isarchiofld  33175  esumcvg  34120  bnj1468  34879  loop1cycl  35202  erdsze2lem2  35269  btwnexch  36090  btwncolinear2  36135  btwncolinear3  36136  btwncolinear4  36137  btwncolinear5  36138  btwncolinear6  36139  nn0prpw  36388  cldbnd  36391  onsuct0  36506  onint1  36514  bj-ceqsalt0  36949  bj-ceqsalt1  36950  bj-inftyexpiinj  37274  bj-bary1lem1  37376  bj-bary1  37377  relowlssretop  37428  isinf2  37470  ltflcei  37668  tan2h  37672  poimirlem26  37706  poimirlem31  37711  ftc1anclem6  37758  dvasin  37764  dvacos  37765  fdc  37805  caushft  37821  heibor1lem  37869  bfplem2  37883  rrncmslem  37892  rngosn3  37984  mpobi123f  38222  riotasv3d  39079  lsatcv1  39167  lub0N  39308  glb0N  39312  oplecon3b  39319  cmtbr4N  39374  cvrnbtwn2  39394  atnlt  39432  atlatle  39439  cvlsupr2  39462  cvrexchlem  39538  cvratlem  39540  atcvrj0  39547  cvrat4  39562  cvrat42  39563  4noncolr3  39572  ps-1  39596  llnnlt  39642  lplnnlt  39684  lvolnltN  39737  dalempnes  39770  dalemqnet  39771  dalem-cly  39790  dalem44  39835  pmaple  39880  cdlemblem  39912  paddss  39964  2polcon4bN  40037  ltrneq2  40267  cdlemc3  40312  cdleme11h  40385  cdleme16b  40398  cdlemednpq  40418  tendospcanN  41142  dihmeetlem13N  41438  mapdordlem2  41756  mapdn0  41788  rspcsbnea  42244  ccatcan2d  42369  ctbnfien  42935  rmxypairf1o  43028  monotoddzzfi  43059  oddcomabszz  43061  acongtr  43095  onsupnmax  43345  onsupsucismax  43396  frege124d  43878  expgrowth  44452  sbcbi  44656  limsupmnflem  45842  funressnfv  47167  funfocofob  47202  2elfz2melfz  47442  iccpartnel  47562  requad2  47747  grlictr  48139  gpg5nbgrvtx13starlem1  48195  gpg5nbgrvtx13starlem3  48197  uzlidlring  48359  ply1mulgsumlem2  48512  fllog2  48693  dignn0flhalflem1  48740