Theorem sylibd 240

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 230	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  3imtr3d  294  csbiebt  3867  rspcsbela  4373  sneqrg  4777  preq1b  4784  csbexg  5239  elrnrexdm  7037  isoselem  7292  funeldmb  7310  riotass2  7350  ordzsl  7792  resf1extb  7881  oaword2  8485  oaordex  8490  omword1  8505  om00  8507  omeulem2  8515  oen0  8519  oeeui  8535  nnaordex  8571  php3  9140  frfi  9192  infglb  9401  suc11reg  9538  cardne  9887  cardsdomel  9896  carduni  9903  acndom  9971  alephinit  10015  cfflb  10179  cfslb2n  10188  fin23lem28  10260  isf34lem6  10300  fin1a2lem9  10328  axcc3  10358  winalim2  10617  inar1  10696  rankcf  10698  addclprlem2  10938  mulclprlem  10940  ltexprlem7  10963  prlem936  10968  reclem4pr  10971  sqgt0sr  11027  ltord2  11677  leord2  11678  eqord2  11679  mulgt1OLD  12012  mulge0b  12024  lt2halves  12410  addltmul  12411  ltsubnn0  12486  nzadd  12573  zextlt  12601  recnz  12602  zeo  12613  peano5uzi  12616  uzm1  12820  irradd  12921  irrmul  12922  xltneg  13167  xleadd1  13205  xmulasslem  13235  xlemul1a  13238  xlemul1  13240  fznuz  13561  uznfz  13562  axdc4uzlem  13943  facndiv  14248  hashvnfin  14320  hashgt12el  14382  hashgt12el2  14383  hashf1  14417  ccatalpha  14554  swrdccatin2  14689  swrdccatin2d  14704  rennim  15199  cau3lem  15315  caubnd2  15318  o1lo1  15497  climrlim2  15507  climshft  15536  subcn2  15555  mulcn2  15556  rlimo1  15577  o1dif  15590  isercoll  15628  caucvgrlem  15633  serf0  15641  cvgrat  15846  efieq1re  16164  moddvds  16230  dvdsssfz1  16285  smuval2  16449  nn0seqcvgd  16537  algcvgblem  16544  eucalglt  16552  lcmgcdlem  16573  rpmul  16626  divgcdcoprm0  16632  isprm6  16682  rpexp  16690  eulerthlem2  16750  prmdiv  16753  pcprendvds2  16810  pcz  16850  pcprmpw  16852  pcadd2  16859  pcfac  16868  expnprm  16871  ramlb  16988  firest  17393  joineu  18344  meeteu  18358  latjlej1  18417  latjlej2  18418  latmlem1  18433  latmlem2  18434  lubun  18479  acsmapd  18518  imasgrp2  19029  issubg4  19119  psgnunilem4  19470  oddvdsnn0  19517  odmulgeq  19530  subgpgp  19570  odcau  19577  lsmlub  19637  frgpnabllem1  19846  pgpfac1lem2  20050  pgpfac1lem3a  20051  pgpfac1lem3  20052  irredrmul  20405  isdomn4  20695  islmhm2  21035  lsmelval2  21082  lspsnat  21145  znidomb  21543  ip2eq  21635  lsmcss  21674  cnpnei  23254  cncls2  23263  cncls  23264  cnntr  23265  cnt0  23336  isnrm2  23348  comppfsc  23522  kqcldsat  23723  isr0  23727  hmeoopn  23756  hmeocld  23757  trufil  23900  opnsubg  24098  ghmcnp  24105  tgphaus  24107  qustgpopn  24110  tsmsgsum  24129  isngp4  24602  xrhmeo  24938  bndth  24950  cfilres  25288  caubl  25300  ivthlem2  25444  ovolicc2  25514  ismbf3d  25646  itg1ge0a  25703  mbfi1flim  25715  itg2gt0  25752  dvge0  25998  dvcnvrelem1  26009  dvcvx  26012  mdegmullem  26068  ig1peu  26165  plyco  26231  coemulc  26245  dgreq0  26255  dgrlt  26256  plymul0or  26272  plydiveu  26289  quotcan  26300  aalioulem3  26325  ulmcaulem  26384  sincosq3sgn  26489  sincosq4sgn  26490  sineq0  26513  logrec  26752  xrlimcnp  26957  cxploglim  26966  lgamgulmlem1  27017  mumul  27169  chtub  27200  perfect1  27216  dchrelbas3  27226  lgsdir2lem4  27316  lgsne0  27323  lgsquad2lem2  27373  2sqlem8a  27413  2sqblem  27419  nogt01o  27685  ltslpss  27925  ltadds2im  28003  ltnegs  28062  z12bday  28502  axcontlem2  29059  elntg2  29079  redwlklem  29763  redwlk  29764  crctcshwlkn0lem3  29905  crctcshwlkn0lem5  29907  clwwlkext2edg  30151  wwlksubclwwlk  30153  frgrwopregasn  30411  frgrwopregbsn  30412  blocnilem  30900  ip2eqi  30952  ubthlem2  30967  hial0  31198  hial02  31199  hial2eq  31202  h1datomi  31677  sumspansn  31745  lnopcnbd  32132  riesz4i  32159  bra11  32204  pjss2coi  32260  pjnormssi  32264  pjorthcoi  32265  pjclem4a  32294  pj3lem1  32302  pj3cor1i  32305  hst1h  32323  stm1i  32339  strlem1  32346  golem2  32368  mdbr2  32392  dmdbr5  32404  mdsl2i  32418  atexch  32477  atcvatlem  32481  chirredlem1  32486  cdjreui  32528  cdj1i  32529  cdj3lem1  32530  xraddge02  32856  submarchi  33274  isarchiofld  33287  esumcvg  34277  bnj1468  35035  loop1cycl  35372  erdsze2lem2  35439  btwnexch  36260  btwncolinear2  36305  btwncolinear3  36306  btwncolinear4  36307  btwncolinear5  36308  btwncolinear6  36309  nn0prpw  36558  cldbnd  36561  onsuct0  36676  onint1  36684  bj-ceqsalt0  37244  bj-ceqsalt1  37245  bj-inftyexpiinj  37576  bj-bary1lem1  37678  bj-bary1  37679  relowlssretop  37732  isinf2  37774  ltflcei  37982  tan2h  37986  poimirlem26  38020  poimirlem31  38025  ftc1anclem6  38072  dvasin  38078  dvacos  38079  fdc  38119  caushft  38135  heibor1lem  38183  bfplem2  38197  rrncmslem  38206  rngosn3  38298  mpobi123f  38536  riotasv3d  39459  lsatcv1  39547  lub0N  39688  glb0N  39692  oplecon3b  39699  cmtbr4N  39754  cvrnbtwn2  39774  atnlt  39812  atlatle  39819  cvlsupr2  39842  cvrexchlem  39918  cvratlem  39920  atcvrj0  39927  cvrat4  39942  cvrat42  39943  4noncolr3  39952  ps-1  39976  llnnlt  40022  lplnnlt  40064  lvolnltN  40117  dalempnes  40150  dalemqnet  40151  dalem-cly  40170  dalem44  40215  pmaple  40260  cdlemblem  40292  paddss  40344  2polcon4bN  40417  ltrneq2  40647  cdlemc3  40692  cdleme11h  40765  cdleme16b  40778  cdlemednpq  40798  tendospcanN  41522  dihmeetlem13N  41818  mapdordlem2  42136  mapdn0  42168  rspcsbnea  42623  ccatcan2d  42742  ctbnfien  43270  rmxypairf1o  43363  monotoddzzfi  43394  oddcomabszz  43396  acongtr  43430  onsupnmax  43680  onsupsucismax  43731  frege124d  44212  expgrowth  44786  sbcbi  44990  limsupmnflem  46170  funressnfv  47513  funfocofob  47548  2elfz2melfz  47788  iccpartnel  47920  requad2  48121  grlictr  48513  gpg5nbgrvtx13starlem1  48569  gpg5nbgrvtx13starlem3  48571  uzlidlring  48733  ply1mulgsumlem2  48885  fllog2  49066  dignn0flhalflem1  49113