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  3903  rspcsbela  4413  sneqrg  4815  preq1b  4822  csbexg  5280  elrnrexdm  7078  isoselem  7333  funeldmb  7351  riotass2  7390  ordzsl  7838  resf1extb  7928  oaword2  8563  oaordex  8568  omword1  8583  om00  8585  omeulem2  8593  oen0  8596  oeeui  8612  nnaordex  8648  php3  9221  php3OLD  9231  onomeneqOLD  9236  frfi  9291  infglb  9501  suc11reg  9631  cardne  9977  cardsdomel  9986  carduni  9993  acndom  10063  alephinit  10107  cfflb  10271  cfslb2n  10280  fin23lem28  10352  isf34lem6  10392  fin1a2lem9  10420  axcc3  10450  winalim2  10708  inar1  10787  rankcf  10789  addclprlem2  11029  mulclprlem  11031  ltexprlem7  11054  prlem936  11059  reclem4pr  11062  sqgt0sr  11118  ltord2  11764  leord2  11765  eqord2  11766  mulgt1OLD  12098  mulge0b  12110  lt2halves  12474  addltmul  12475  ltsubnn0  12550  nzadd  12638  zextlt  12665  recnz  12666  zeo  12677  peano5uzi  12680  uzm1  12888  irradd  12987  irrmul  12988  xltneg  13231  xleadd1  13269  xmulasslem  13299  xlemul1a  13302  xlemul1  13304  fznuz  13624  uznfz  13625  axdc4uzlem  13999  facndiv  14304  hashvnfin  14376  hashgt12el  14438  hashgt12el2  14439  hashf1  14473  ccatalpha  14609  swrdccatin2  14745  swrdccatin2d  14760  rennim  15256  cau3lem  15371  caubnd2  15374  o1lo1  15551  climrlim2  15561  climshft  15590  subcn2  15609  mulcn2  15610  rlimo1  15631  o1dif  15644  isercoll  15682  caucvgrlem  15687  serf0  15695  cvgrat  15897  efieq1re  16215  moddvds  16281  dvdsssfz1  16335  smuval2  16499  nn0seqcvgd  16587  algcvgblem  16594  eucalglt  16602  lcmgcdlem  16623  rpmul  16676  divgcdcoprm0  16682  isprm6  16731  rpexp  16739  eulerthlem2  16799  prmdiv  16802  pcprendvds2  16859  pcz  16899  pcprmpw  16901  pcadd2  16908  pcfac  16917  expnprm  16920  ramlb  17037  firest  17444  joineu  18390  meeteu  18404  latjlej1  18461  latjlej2  18462  latmlem1  18477  latmlem2  18478  lubun  18523  acsmapd  18562  imasgrp2  19036  issubg4  19126  psgnunilem4  19476  oddvdsnn0  19523  odmulgeq  19536  subgpgp  19576  odcau  19583  lsmlub  19643  frgpnabllem1  19852  pgpfac1lem2  20056  pgpfac1lem3a  20057  pgpfac1lem3  20058  irredrmul  20385  isdomn4  20674  islmhm2  20994  lsmelval2  21041  lspsnat  21104  znidomb  21520  ip2eq  21611  lsmcss  21650  cnpnei  23200  cncls2  23209  cncls  23210  cnntr  23211  cnt0  23282  isnrm2  23294  comppfsc  23468  kqcldsat  23669  isr0  23673  hmeoopn  23702  hmeocld  23703  trufil  23846  opnsubg  24044  ghmcnp  24051  tgphaus  24053  qustgpopn  24056  tsmsgsum  24075  isngp4  24549  xrhmeo  24893  bndth  24906  cfilres  25246  caubl  25258  ivthlem2  25403  ovolicc2  25473  ismbf3d  25605  itg1ge0a  25662  mbfi1flim  25674  itg2gt0  25711  dvge0  25961  dvcnvrelem1  25972  dvcvx  25975  mdegmullem  26033  ig1peu  26130  plyco  26196  coemulc  26210  dgreq0  26221  dgrlt  26222  plymul0or  26238  plydiveu  26256  quotcan  26267  aalioulem3  26292  ulmcaulem  26353  sincosq3sgn  26459  sincosq4sgn  26460  sineq0  26483  logrec  26723  xrlimcnp  26928  cxploglim  26938  lgamgulmlem1  26989  mumul  27141  chtub  27173  perfect1  27189  dchrelbas3  27199  lgsdir2lem4  27289  lgsne0  27296  lgsquad2lem2  27346  2sqlem8a  27386  2sqblem  27392  nogt01o  27658  sltlpss  27862  sltadd2im  27936  sltneg  27994  axcontlem2  28890  elntg2  28910  redwlklem  29597  redwlk  29598  crctcshwlkn0lem3  29740  crctcshwlkn0lem5  29742  clwwlkext2edg  29983  wwlksubclwwlk  29985  frgrwopregasn  30243  frgrwopregbsn  30244  blocnilem  30731  ip2eqi  30783  ubthlem2  30798  hial0  31029  hial02  31030  hial2eq  31033  h1datomi  31508  sumspansn  31576  lnopcnbd  31963  riesz4i  31990  bra11  32035  pjss2coi  32091  pjnormssi  32095  pjorthcoi  32096  pjclem4a  32125  pj3lem1  32133  pj3cor1i  32136  hst1h  32154  stm1i  32170  strlem1  32177  golem2  32199  mdbr2  32223  dmdbr5  32235  mdsl2i  32249  atexch  32308  atcvatlem  32312  chirredlem1  32317  cdjreui  32359  cdj1i  32360  cdj3lem1  32361  xraddge02  32680  submarchi  33130  isarchiofld  33285  esumcvg  34063  bnj1468  34823  loop1cycl  35105  erdsze2lem2  35172  btwnexch  35989  btwncolinear2  36034  btwncolinear3  36035  btwncolinear4  36036  btwncolinear5  36037  btwncolinear6  36038  nn0prpw  36287  cldbnd  36290  onsuct0  36405  onint1  36413  bj-ceqsalt0  36848  bj-ceqsalt1  36849  bj-inftyexpiinj  37173  bj-bary1lem1  37275  bj-bary1  37276  relowlssretop  37327  isinf2  37369  ltflcei  37578  tan2h  37582  poimirlem26  37616  poimirlem31  37621  ftc1anclem6  37668  dvasin  37674  dvacos  37675  fdc  37715  caushft  37731  heibor1lem  37779  bfplem2  37793  rrncmslem  37802  rngosn3  37894  mpobi123f  38132  riotasv3d  38924  lsatcv1  39012  lub0N  39153  glb0N  39157  oplecon3b  39164  cmtbr4N  39219  cvrnbtwn2  39239  atnlt  39277  atlatle  39284  cvlsupr2  39307  cvrexchlem  39384  cvratlem  39386  atcvrj0  39393  cvrat4  39408  cvrat42  39409  4noncolr3  39418  ps-1  39442  llnnlt  39488  lplnnlt  39530  lvolnltN  39583  dalempnes  39616  dalemqnet  39617  dalem-cly  39636  dalem44  39681  pmaple  39726  cdlemblem  39758  paddss  39810  2polcon4bN  39883  ltrneq2  40113  cdlemc3  40158  cdleme11h  40231  cdleme16b  40244  cdlemednpq  40264  tendospcanN  40988  dihmeetlem13N  41284  mapdordlem2  41602  mapdn0  41634  rspcsbnea  42090  ccatcan2d  42249  ctbnfien  42788  rmxypairf1o  42882  monotoddzzfi  42913  oddcomabszz  42915  acongtr  42949  onsupnmax  43199  onsupsucismax  43250  frege124d  43732  expgrowth  44307  sbcbi  44512  limsupmnflem  45697  funressnfv  47020  funfocofob  47055  2elfz2melfz  47295  iccpartnel  47400  requad2  47585  grlictr  47968  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem3  48023  uzlidlring  48158  ply1mulgsumlem2  48311  fllog2  48496  dignn0flhalflem1  48543