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  sbceqalOLD  3857  csbiebt  3937  rspcsbela  4443  sneqrg  4843  preq1b  4850  csbexg  5315  elrnrexdm  7108  isoselem  7360  funeldmb  7378  riotass2  7417  ordzsl  7865  oaword2  8589  oaordex  8594  omword1  8609  om00  8611  omeulem2  8619  oen0  8622  oeeui  8638  nnaordex  8674  php3  9246  php3OLD  9258  onomeneqOLD  9263  frfi  9318  infglb  9527  suc11reg  9656  cardne  10002  cardsdomel  10011  carduni  10018  acndom  10088  alephinit  10132  cfflb  10296  cfslb2n  10305  fin23lem28  10377  isf34lem6  10417  fin1a2lem9  10445  axcc3  10475  winalim2  10733  inar1  10812  rankcf  10814  addclprlem2  11054  mulclprlem  11056  ltexprlem7  11079  prlem936  11084  reclem4pr  11087  sqgt0sr  11143  ltord2  11789  leord2  11790  eqord2  11791  mulgt1OLD  12123  mulge0b  12135  lt2halves  12498  addltmul  12499  ltsubnn0  12574  nzadd  12662  zextlt  12689  recnz  12690  zeo  12701  peano5uzi  12704  uzm1  12913  irradd  13012  irrmul  13013  xltneg  13255  xleadd1  13293  xmulasslem  13323  xlemul1a  13326  xlemul1  13328  fznuz  13645  uznfz  13646  axdc4uzlem  14020  facndiv  14323  hashvnfin  14395  hashgt12el  14457  hashgt12el2  14458  hashf1  14492  ccatalpha  14627  swrdccatin2  14763  swrdccatin2d  14778  rennim  15274  cau3lem  15389  caubnd2  15392  o1lo1  15569  climrlim2  15579  climshft  15608  subcn2  15627  mulcn2  15628  rlimo1  15649  o1dif  15662  isercoll  15700  caucvgrlem  15705  serf0  15713  cvgrat  15915  efieq1re  16231  moddvds  16297  dvdsssfz1  16351  smuval2  16515  nn0seqcvgd  16603  algcvgblem  16610  eucalglt  16618  lcmgcdlem  16639  rpmul  16692  divgcdcoprm0  16698  isprm6  16747  rpexp  16755  eulerthlem2  16815  prmdiv  16818  pcprendvds2  16874  pcz  16914  pcprmpw  16916  pcadd2  16923  pcfac  16932  expnprm  16935  ramlb  17052  firest  17478  joineu  18439  meeteu  18453  latjlej1  18510  latjlej2  18511  latmlem1  18526  latmlem2  18527  lubun  18572  acsmapd  18611  imasgrp2  19085  issubg4  19175  psgnunilem4  19529  oddvdsnn0  19576  odmulgeq  19589  subgpgp  19629  odcau  19636  lsmlub  19696  frgpnabllem1  19905  pgpfac1lem2  20109  pgpfac1lem3a  20110  pgpfac1lem3  20111  irredrmul  20443  isdomn4  20732  islmhm2  21054  lsmelval2  21101  lspsnat  21164  znidomb  21597  ip2eq  21688  lsmcss  21727  cnpnei  23287  cncls2  23296  cncls  23297  cnntr  23298  cnt0  23369  isnrm2  23381  comppfsc  23555  kqcldsat  23756  isr0  23760  hmeoopn  23789  hmeocld  23790  trufil  23933  opnsubg  24131  ghmcnp  24138  tgphaus  24140  qustgpopn  24143  tsmsgsum  24162  isngp4  24640  xrhmeo  24990  bndth  25003  cfilres  25343  caubl  25355  ivthlem2  25500  ovolicc2  25570  ismbf3d  25702  itg1ge0a  25760  mbfi1flim  25772  itg2gt0  25809  dvge0  26059  dvcnvrelem1  26070  dvcvx  26073  mdegmullem  26131  ig1peu  26228  plyco  26294  coemulc  26308  dgreq0  26319  dgrlt  26320  plymul0or  26336  plydiveu  26354  quotcan  26365  aalioulem3  26390  ulmcaulem  26451  sincosq3sgn  26556  sincosq4sgn  26557  sineq0  26580  logrec  26820  xrlimcnp  27025  cxploglim  27035  lgamgulmlem1  27086  mumul  27238  chtub  27270  perfect1  27286  dchrelbas3  27296  lgsdir2lem4  27386  lgsne0  27393  lgsquad2lem2  27443  2sqlem8a  27483  2sqblem  27489  nogt01o  27755  sltlpss  27959  sltadd2im  28033  sltneg  28091  axcontlem2  28994  elntg2  29014  redwlklem  29703  redwlk  29704  crctcshwlkn0lem3  29841  crctcshwlkn0lem5  29843  clwwlkext2edg  30084  wwlksubclwwlk  30086  frgrwopregasn  30344  frgrwopregbsn  30345  blocnilem  30832  ip2eqi  30884  ubthlem2  30899  hial0  31130  hial02  31131  hial2eq  31134  h1datomi  31609  sumspansn  31677  lnopcnbd  32064  riesz4i  32091  bra11  32136  pjss2coi  32192  pjnormssi  32196  pjorthcoi  32197  pjclem4a  32226  pj3lem1  32234  pj3cor1i  32237  hst1h  32255  stm1i  32271  strlem1  32278  golem2  32300  mdbr2  32324  dmdbr5  32336  mdsl2i  32350  atexch  32409  atcvatlem  32413  chirredlem1  32418  cdjreui  32460  cdj1i  32461  cdj3lem1  32462  xraddge02  32766  submarchi  33175  isarchiofld  33326  esumcvg  34066  bnj1468  34838  loop1cycl  35121  erdsze2lem2  35188  btwnexch  36006  btwncolinear2  36051  btwncolinear3  36052  btwncolinear4  36053  btwncolinear5  36054  btwncolinear6  36055  nn0prpw  36305  cldbnd  36308  onsuct0  36423  onint1  36431  bj-ceqsalt0  36866  bj-ceqsalt1  36867  bj-inftyexpiinj  37191  bj-bary1lem1  37293  bj-bary1  37294  relowlssretop  37345  isinf2  37387  ltflcei  37594  tan2h  37598  poimirlem26  37632  poimirlem31  37637  ftc1anclem6  37684  dvasin  37690  dvacos  37691  fdc  37731  caushft  37747  heibor1lem  37795  bfplem2  37809  rrncmslem  37818  rngosn3  37910  mpobi123f  38148  riotasv3d  38941  lsatcv1  39029  lub0N  39170  glb0N  39174  oplecon3b  39181  cmtbr4N  39236  cvrnbtwn2  39256  atnlt  39294  atlatle  39301  cvlsupr2  39324  cvrexchlem  39401  cvratlem  39403  atcvrj0  39410  cvrat4  39425  cvrat42  39426  4noncolr3  39435  ps-1  39459  llnnlt  39505  lplnnlt  39547  lvolnltN  39600  dalempnes  39633  dalemqnet  39634  dalem-cly  39653  dalem44  39698  pmaple  39743  cdlemblem  39775  paddss  39827  2polcon4bN  39900  ltrneq2  40130  cdlemc3  40175  cdleme11h  40248  cdleme16b  40261  cdlemednpq  40281  tendospcanN  41005  dihmeetlem13N  41301  mapdordlem2  41619  mapdn0  41651  rspcsbnea  42112  ccatcan2d  42270  ctbnfien  42805  rmxypairf1o  42899  monotoddzzfi  42930  oddcomabszz  42932  acongtr  42966  onsupnmax  43216  onsupsucismax  43268  frege124d  43750  expgrowth  44330  sbcbi  44536  limsupmnflem  45675  funressnfv  46992  funfocofob  47027  2elfz2melfz  47267  iccpartnel  47362  requad2  47547  grlictr  47910  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem3  47963  uzlidlring  48078  ply1mulgsumlem2  48232  fllog2  48417  dignn0flhalflem1  48464