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  3852  csbiebt  3928  rspcsbela  4438  sneqrg  4839  preq1b  4846  csbexg  5310  elrnrexdm  7109  isoselem  7361  funeldmb  7379  riotass2  7418  ordzsl  7866  resf1extb  7956  oaword2  8591  oaordex  8596  omword1  8611  om00  8613  omeulem2  8621  oen0  8624  oeeui  8640  nnaordex  8676  php3  9249  php3OLD  9261  onomeneqOLD  9266  frfi  9321  infglb  9530  suc11reg  9659  cardne  10005  cardsdomel  10014  carduni  10021  acndom  10091  alephinit  10135  cfflb  10299  cfslb2n  10308  fin23lem28  10380  isf34lem6  10420  fin1a2lem9  10448  axcc3  10478  winalim2  10736  inar1  10815  rankcf  10817  addclprlem2  11057  mulclprlem  11059  ltexprlem7  11082  prlem936  11087  reclem4pr  11090  sqgt0sr  11146  ltord2  11792  leord2  11793  eqord2  11794  mulgt1OLD  12126  mulge0b  12138  lt2halves  12501  addltmul  12502  ltsubnn0  12577  nzadd  12665  zextlt  12692  recnz  12693  zeo  12704  peano5uzi  12707  uzm1  12916  irradd  13015  irrmul  13016  xltneg  13259  xleadd1  13297  xmulasslem  13327  xlemul1a  13330  xlemul1  13332  fznuz  13649  uznfz  13650  axdc4uzlem  14024  facndiv  14327  hashvnfin  14399  hashgt12el  14461  hashgt12el2  14462  hashf1  14496  ccatalpha  14631  swrdccatin2  14767  swrdccatin2d  14782  rennim  15278  cau3lem  15393  caubnd2  15396  o1lo1  15573  climrlim2  15583  climshft  15612  subcn2  15631  mulcn2  15632  rlimo1  15653  o1dif  15666  isercoll  15704  caucvgrlem  15709  serf0  15717  cvgrat  15919  efieq1re  16235  moddvds  16301  dvdsssfz1  16355  smuval2  16519  nn0seqcvgd  16607  algcvgblem  16614  eucalglt  16622  lcmgcdlem  16643  rpmul  16696  divgcdcoprm0  16702  isprm6  16751  rpexp  16759  eulerthlem2  16819  prmdiv  16822  pcprendvds2  16879  pcz  16919  pcprmpw  16921  pcadd2  16928  pcfac  16937  expnprm  16940  ramlb  17057  firest  17477  joineu  18427  meeteu  18441  latjlej1  18498  latjlej2  18499  latmlem1  18514  latmlem2  18515  lubun  18560  acsmapd  18599  imasgrp2  19073  issubg4  19163  psgnunilem4  19515  oddvdsnn0  19562  odmulgeq  19575  subgpgp  19615  odcau  19622  lsmlub  19682  frgpnabllem1  19891  pgpfac1lem2  20095  pgpfac1lem3a  20096  pgpfac1lem3  20097  irredrmul  20427  isdomn4  20716  islmhm2  21037  lsmelval2  21084  lspsnat  21147  znidomb  21580  ip2eq  21671  lsmcss  21710  cnpnei  23272  cncls2  23281  cncls  23282  cnntr  23283  cnt0  23354  isnrm2  23366  comppfsc  23540  kqcldsat  23741  isr0  23745  hmeoopn  23774  hmeocld  23775  trufil  23918  opnsubg  24116  ghmcnp  24123  tgphaus  24125  qustgpopn  24128  tsmsgsum  24147  isngp4  24625  xrhmeo  24977  bndth  24990  cfilres  25330  caubl  25342  ivthlem2  25487  ovolicc2  25557  ismbf3d  25689  itg1ge0a  25746  mbfi1flim  25758  itg2gt0  25795  dvge0  26045  dvcnvrelem1  26056  dvcvx  26059  mdegmullem  26117  ig1peu  26214  plyco  26280  coemulc  26294  dgreq0  26305  dgrlt  26306  plymul0or  26322  plydiveu  26340  quotcan  26351  aalioulem3  26376  ulmcaulem  26437  sincosq3sgn  26542  sincosq4sgn  26543  sineq0  26566  logrec  26806  xrlimcnp  27011  cxploglim  27021  lgamgulmlem1  27072  mumul  27224  chtub  27256  perfect1  27272  dchrelbas3  27282  lgsdir2lem4  27372  lgsne0  27379  lgsquad2lem2  27429  2sqlem8a  27469  2sqblem  27475  nogt01o  27741  sltlpss  27945  sltadd2im  28019  sltneg  28077  axcontlem2  28980  elntg2  29000  redwlklem  29689  redwlk  29690  crctcshwlkn0lem3  29832  crctcshwlkn0lem5  29834  clwwlkext2edg  30075  wwlksubclwwlk  30077  frgrwopregasn  30335  frgrwopregbsn  30336  blocnilem  30823  ip2eqi  30875  ubthlem2  30890  hial0  31121  hial02  31122  hial2eq  31125  h1datomi  31600  sumspansn  31668  lnopcnbd  32055  riesz4i  32082  bra11  32127  pjss2coi  32183  pjnormssi  32187  pjorthcoi  32188  pjclem4a  32217  pj3lem1  32225  pj3cor1i  32228  hst1h  32246  stm1i  32262  strlem1  32269  golem2  32291  mdbr2  32315  dmdbr5  32327  mdsl2i  32341  atexch  32400  atcvatlem  32404  chirredlem1  32409  cdjreui  32451  cdj1i  32452  cdj3lem1  32453  xraddge02  32760  submarchi  33193  isarchiofld  33347  esumcvg  34087  bnj1468  34860  loop1cycl  35142  erdsze2lem2  35209  btwnexch  36026  btwncolinear2  36071  btwncolinear3  36072  btwncolinear4  36073  btwncolinear5  36074  btwncolinear6  36075  nn0prpw  36324  cldbnd  36327  onsuct0  36442  onint1  36450  bj-ceqsalt0  36885  bj-ceqsalt1  36886  bj-inftyexpiinj  37210  bj-bary1lem1  37312  bj-bary1  37313  relowlssretop  37364  isinf2  37406  ltflcei  37615  tan2h  37619  poimirlem26  37653  poimirlem31  37658  ftc1anclem6  37705  dvasin  37711  dvacos  37712  fdc  37752  caushft  37768  heibor1lem  37816  bfplem2  37830  rrncmslem  37839  rngosn3  37931  mpobi123f  38169  riotasv3d  38961  lsatcv1  39049  lub0N  39190  glb0N  39194  oplecon3b  39201  cmtbr4N  39256  cvrnbtwn2  39276  atnlt  39314  atlatle  39321  cvlsupr2  39344  cvrexchlem  39421  cvratlem  39423  atcvrj0  39430  cvrat4  39445  cvrat42  39446  4noncolr3  39455  ps-1  39479  llnnlt  39525  lplnnlt  39567  lvolnltN  39620  dalempnes  39653  dalemqnet  39654  dalem-cly  39673  dalem44  39718  pmaple  39763  cdlemblem  39795  paddss  39847  2polcon4bN  39920  ltrneq2  40150  cdlemc3  40195  cdleme11h  40268  cdleme16b  40281  cdlemednpq  40301  tendospcanN  41025  dihmeetlem13N  41321  mapdordlem2  41639  mapdn0  41671  rspcsbnea  42132  ccatcan2d  42292  ctbnfien  42829  rmxypairf1o  42923  monotoddzzfi  42954  oddcomabszz  42956  acongtr  42990  onsupnmax  43240  onsupsucismax  43292  frege124d  43774  expgrowth  44354  sbcbi  44559  limsupmnflem  45735  funressnfv  47055  funfocofob  47090  2elfz2melfz  47330  iccpartnel  47425  requad2  47610  grlictr  47975  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem3  48029  uzlidlring  48151  ply1mulgsumlem2  48304  fllog2  48489  dignn0flhalflem1  48536