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  3882  rspcsbela  4391  sneqrg  4793  preq1b  4800  csbexg  5252  elrnrexdm  7027  isoselem  7282  funeldmb  7300  riotass2  7340  ordzsl  7785  resf1extb  7874  oaword2  8478  oaordex  8483  omword1  8498  om00  8500  omeulem2  8508  oen0  8511  oeeui  8527  nnaordex  8563  php3  9133  frfi  9190  infglb  9400  suc11reg  9534  cardne  9880  cardsdomel  9889  carduni  9896  acndom  9964  alephinit  10008  cfflb  10172  cfslb2n  10181  fin23lem28  10253  isf34lem6  10293  fin1a2lem9  10321  axcc3  10351  winalim2  10609  inar1  10688  rankcf  10690  addclprlem2  10930  mulclprlem  10932  ltexprlem7  10955  prlem936  10960  reclem4pr  10963  sqgt0sr  11019  ltord2  11667  leord2  11668  eqord2  11669  mulgt1OLD  12001  mulge0b  12013  lt2halves  12377  addltmul  12378  ltsubnn0  12453  nzadd  12541  zextlt  12568  recnz  12569  zeo  12580  peano5uzi  12583  uzm1  12791  irradd  12892  irrmul  12893  xltneg  13137  xleadd1  13175  xmulasslem  13205  xlemul1a  13208  xlemul1  13210  fznuz  13530  uznfz  13531  axdc4uzlem  13908  facndiv  14213  hashvnfin  14285  hashgt12el  14347  hashgt12el2  14348  hashf1  14382  ccatalpha  14518  swrdccatin2  14653  swrdccatin2d  14668  rennim  15164  cau3lem  15280  caubnd2  15283  o1lo1  15462  climrlim2  15472  climshft  15501  subcn2  15520  mulcn2  15521  rlimo1  15542  o1dif  15555  isercoll  15593  caucvgrlem  15598  serf0  15606  cvgrat  15808  efieq1re  16126  moddvds  16192  dvdsssfz1  16247  smuval2  16411  nn0seqcvgd  16499  algcvgblem  16506  eucalglt  16514  lcmgcdlem  16535  rpmul  16588  divgcdcoprm0  16594  isprm6  16643  rpexp  16651  eulerthlem2  16711  prmdiv  16714  pcprendvds2  16771  pcz  16811  pcprmpw  16813  pcadd2  16820  pcfac  16829  expnprm  16832  ramlb  16949  firest  17354  joineu  18304  meeteu  18318  latjlej1  18377  latjlej2  18378  latmlem1  18393  latmlem2  18394  lubun  18439  acsmapd  18478  imasgrp2  18952  issubg4  19042  psgnunilem4  19394  oddvdsnn0  19441  odmulgeq  19454  subgpgp  19494  odcau  19501  lsmlub  19561  frgpnabllem1  19770  pgpfac1lem2  19974  pgpfac1lem3a  19975  pgpfac1lem3  19976  irredrmul  20330  isdomn4  20619  islmhm2  20960  lsmelval2  21007  lspsnat  21070  znidomb  21486  ip2eq  21578  lsmcss  21617  cnpnei  23167  cncls2  23176  cncls  23177  cnntr  23178  cnt0  23249  isnrm2  23261  comppfsc  23435  kqcldsat  23636  isr0  23640  hmeoopn  23669  hmeocld  23670  trufil  23813  opnsubg  24011  ghmcnp  24018  tgphaus  24020  qustgpopn  24023  tsmsgsum  24042  isngp4  24516  xrhmeo  24860  bndth  24873  cfilres  25212  caubl  25224  ivthlem2  25369  ovolicc2  25439  ismbf3d  25571  itg1ge0a  25628  mbfi1flim  25640  itg2gt0  25677  dvge0  25927  dvcnvrelem1  25938  dvcvx  25941  mdegmullem  25999  ig1peu  26096  plyco  26162  coemulc  26176  dgreq0  26187  dgrlt  26188  plymul0or  26204  plydiveu  26222  quotcan  26233  aalioulem3  26258  ulmcaulem  26319  sincosq3sgn  26425  sincosq4sgn  26426  sineq0  26449  logrec  26689  xrlimcnp  26894  cxploglim  26904  lgamgulmlem1  26955  mumul  27107  chtub  27139  perfect1  27155  dchrelbas3  27165  lgsdir2lem4  27255  lgsne0  27262  lgsquad2lem2  27312  2sqlem8a  27352  2sqblem  27358  nogt01o  27624  sltlpss  27840  sltadd2im  27916  sltneg  27974  axcontlem2  28928  elntg2  28948  redwlklem  29633  redwlk  29634  crctcshwlkn0lem3  29775  crctcshwlkn0lem5  29777  clwwlkext2edg  30018  wwlksubclwwlk  30020  frgrwopregasn  30278  frgrwopregbsn  30279  blocnilem  30766  ip2eqi  30818  ubthlem2  30833  hial0  31064  hial02  31065  hial2eq  31068  h1datomi  31543  sumspansn  31611  lnopcnbd  31998  riesz4i  32025  bra11  32070  pjss2coi  32126  pjnormssi  32130  pjorthcoi  32131  pjclem4a  32160  pj3lem1  32168  pj3cor1i  32171  hst1h  32189  stm1i  32205  strlem1  32212  golem2  32234  mdbr2  32258  dmdbr5  32270  mdsl2i  32284  atexch  32343  atcvatlem  32347  chirredlem1  32352  cdjreui  32394  cdj1i  32395  cdj3lem1  32396  xraddge02  32713  submarchi  33138  isarchiofld  33151  esumcvg  34052  bnj1468  34812  loop1cycl  35109  erdsze2lem2  35176  btwnexch  35998  btwncolinear2  36043  btwncolinear3  36044  btwncolinear4  36045  btwncolinear5  36046  btwncolinear6  36047  nn0prpw  36296  cldbnd  36299  onsuct0  36414  onint1  36422  bj-ceqsalt0  36857  bj-ceqsalt1  36858  bj-inftyexpiinj  37182  bj-bary1lem1  37284  bj-bary1  37285  relowlssretop  37336  isinf2  37378  ltflcei  37587  tan2h  37591  poimirlem26  37625  poimirlem31  37630  ftc1anclem6  37677  dvasin  37683  dvacos  37684  fdc  37724  caushft  37740  heibor1lem  37788  bfplem2  37802  rrncmslem  37811  rngosn3  37903  mpobi123f  38141  riotasv3d  38938  lsatcv1  39026  lub0N  39167  glb0N  39171  oplecon3b  39178  cmtbr4N  39233  cvrnbtwn2  39253  atnlt  39291  atlatle  39298  cvlsupr2  39321  cvrexchlem  39398  cvratlem  39400  atcvrj0  39407  cvrat4  39422  cvrat42  39423  4noncolr3  39432  ps-1  39456  llnnlt  39502  lplnnlt  39544  lvolnltN  39597  dalempnes  39630  dalemqnet  39631  dalem-cly  39650  dalem44  39695  pmaple  39740  cdlemblem  39772  paddss  39824  2polcon4bN  39897  ltrneq2  40127  cdlemc3  40172  cdleme11h  40245  cdleme16b  40258  cdlemednpq  40278  tendospcanN  41002  dihmeetlem13N  41298  mapdordlem2  41616  mapdn0  41648  rspcsbnea  42104  ccatcan2d  42224  ctbnfien  42791  rmxypairf1o  42884  monotoddzzfi  42915  oddcomabszz  42917  acongtr  42951  onsupnmax  43201  onsupsucismax  43252  frege124d  43734  expgrowth  44308  sbcbi  44513  limsupmnflem  45702  funressnfv  47028  funfocofob  47063  2elfz2melfz  47303  iccpartnel  47423  requad2  47608  grlictr  48000  gpg5nbgrvtx13starlem1  48056  gpg5nbgrvtx13starlem3  48058  uzlidlring  48220  ply1mulgsumlem2  48373  fllog2  48554  dignn0flhalflem1  48601