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  3880  rspcsbela  4392  sneqrg  4797  preq1b  4804  csbexg  5257  elrnrexdm  7043  isoselem  7297  funeldmb  7315  riotass2  7355  ordzsl  7797  resf1extb  7886  oaword2  8490  oaordex  8495  omword1  8510  om00  8512  omeulem2  8520  oen0  8524  oeeui  8540  nnaordex  8576  php3  9145  frfi  9197  infglb  9406  suc11reg  9540  cardne  9889  cardsdomel  9898  carduni  9905  acndom  9973  alephinit  10017  cfflb  10181  cfslb2n  10190  fin23lem28  10262  isf34lem6  10302  fin1a2lem9  10330  axcc3  10360  winalim2  10619  inar1  10698  rankcf  10700  addclprlem2  10940  mulclprlem  10942  ltexprlem7  10965  prlem936  10970  reclem4pr  10973  sqgt0sr  11029  ltord2  11678  leord2  11679  eqord2  11680  mulgt1OLD  12012  mulge0b  12024  lt2halves  12388  addltmul  12389  ltsubnn0  12464  nzadd  12551  zextlt  12578  recnz  12579  zeo  12590  peano5uzi  12593  uzm1  12797  irradd  12898  irrmul  12899  xltneg  13144  xleadd1  13182  xmulasslem  13212  xlemul1a  13215  xlemul1  13217  fznuz  13537  uznfz  13538  axdc4uzlem  13918  facndiv  14223  hashvnfin  14295  hashgt12el  14357  hashgt12el2  14358  hashf1  14392  ccatalpha  14529  swrdccatin2  14664  swrdccatin2d  14679  rennim  15174  cau3lem  15290  caubnd2  15293  o1lo1  15472  climrlim2  15482  climshft  15511  subcn2  15530  mulcn2  15531  rlimo1  15552  o1dif  15565  isercoll  15603  caucvgrlem  15608  serf0  15616  cvgrat  15818  efieq1re  16136  moddvds  16202  dvdsssfz1  16257  smuval2  16421  nn0seqcvgd  16509  algcvgblem  16516  eucalglt  16524  lcmgcdlem  16545  rpmul  16598  divgcdcoprm0  16604  isprm6  16653  rpexp  16661  eulerthlem2  16721  prmdiv  16724  pcprendvds2  16781  pcz  16821  pcprmpw  16823  pcadd2  16830  pcfac  16839  expnprm  16842  ramlb  16959  firest  17364  joineu  18315  meeteu  18329  latjlej1  18388  latjlej2  18389  latmlem1  18404  latmlem2  18405  lubun  18450  acsmapd  18489  imasgrp2  18997  issubg4  19087  psgnunilem4  19438  oddvdsnn0  19485  odmulgeq  19498  subgpgp  19538  odcau  19545  lsmlub  19605  frgpnabllem1  19814  pgpfac1lem2  20018  pgpfac1lem3a  20019  pgpfac1lem3  20020  irredrmul  20375  isdomn4  20661  islmhm2  21002  lsmelval2  21049  lspsnat  21112  znidomb  21528  ip2eq  21620  lsmcss  21659  cnpnei  23220  cncls2  23229  cncls  23230  cnntr  23231  cnt0  23302  isnrm2  23314  comppfsc  23488  kqcldsat  23689  isr0  23693  hmeoopn  23722  hmeocld  23723  trufil  23866  opnsubg  24064  ghmcnp  24071  tgphaus  24073  qustgpopn  24076  tsmsgsum  24095  isngp4  24568  xrhmeo  24912  bndth  24925  cfilres  25264  caubl  25276  ivthlem2  25421  ovolicc2  25491  ismbf3d  25623  itg1ge0a  25680  mbfi1flim  25692  itg2gt0  25729  dvge0  25979  dvcnvrelem1  25990  dvcvx  25993  mdegmullem  26051  ig1peu  26148  plyco  26214  coemulc  26228  dgreq0  26239  dgrlt  26240  plymul0or  26256  plydiveu  26274  quotcan  26285  aalioulem3  26310  ulmcaulem  26371  sincosq3sgn  26477  sincosq4sgn  26478  sineq0  26501  logrec  26741  xrlimcnp  26946  cxploglim  26956  lgamgulmlem1  27007  mumul  27159  chtub  27191  perfect1  27207  dchrelbas3  27217  lgsdir2lem4  27307  lgsne0  27314  lgsquad2lem2  27364  2sqlem8a  27404  2sqblem  27410  nogt01o  27676  ltslpss  27916  ltadds2im  27994  ltnegs  28053  z12bday  28493  axcontlem2  29050  elntg2  29070  redwlklem  29755  redwlk  29756  crctcshwlkn0lem3  29897  crctcshwlkn0lem5  29899  clwwlkext2edg  30143  wwlksubclwwlk  30145  frgrwopregasn  30403  frgrwopregbsn  30404  blocnilem  30891  ip2eqi  30943  ubthlem2  30958  hial0  31189  hial02  31190  hial2eq  31193  h1datomi  31668  sumspansn  31736  lnopcnbd  32123  riesz4i  32150  bra11  32195  pjss2coi  32251  pjnormssi  32255  pjorthcoi  32256  pjclem4a  32285  pj3lem1  32293  pj3cor1i  32296  hst1h  32314  stm1i  32330  strlem1  32337  golem2  32359  mdbr2  32383  dmdbr5  32395  mdsl2i  32409  atexch  32468  atcvatlem  32472  chirredlem1  32477  cdjreui  32519  cdj1i  32520  cdj3lem1  32521  xraddge02  32847  submarchi  33279  isarchiofld  33292  esumcvg  34263  bnj1468  35021  loop1cycl  35350  erdsze2lem2  35417  btwnexch  36238  btwncolinear2  36283  btwncolinear3  36284  btwncolinear4  36285  btwncolinear5  36286  btwncolinear6  36287  nn0prpw  36536  cldbnd  36539  onsuct0  36654  onint1  36662  bj-ceqsalt0  37126  bj-ceqsalt1  37127  bj-inftyexpiinj  37458  bj-bary1lem1  37560  bj-bary1  37561  relowlssretop  37612  isinf2  37654  ltflcei  37853  tan2h  37857  poimirlem26  37891  poimirlem31  37896  ftc1anclem6  37943  dvasin  37949  dvacos  37950  fdc  37990  caushft  38006  heibor1lem  38054  bfplem2  38068  rrncmslem  38077  rngosn3  38169  mpobi123f  38407  riotasv3d  39330  lsatcv1  39418  lub0N  39559  glb0N  39563  oplecon3b  39570  cmtbr4N  39625  cvrnbtwn2  39645  atnlt  39683  atlatle  39690  cvlsupr2  39713  cvrexchlem  39789  cvratlem  39791  atcvrj0  39798  cvrat4  39813  cvrat42  39814  4noncolr3  39823  ps-1  39847  llnnlt  39893  lplnnlt  39935  lvolnltN  39988  dalempnes  40021  dalemqnet  40022  dalem-cly  40041  dalem44  40086  pmaple  40131  cdlemblem  40163  paddss  40215  2polcon4bN  40288  ltrneq2  40518  cdlemc3  40563  cdleme11h  40636  cdleme16b  40649  cdlemednpq  40669  tendospcanN  41393  dihmeetlem13N  41689  mapdordlem2  42007  mapdn0  42039  rspcsbnea  42495  ccatcan2d  42615  ctbnfien  43169  rmxypairf1o  43262  monotoddzzfi  43293  oddcomabszz  43295  acongtr  43329  onsupnmax  43579  onsupsucismax  43630  frege124d  44111  expgrowth  44685  sbcbi  44889  limsupmnflem  46072  funressnfv  47397  funfocofob  47432  2elfz2melfz  47672  iccpartnel  47792  requad2  47977  grlictr  48369  gpg5nbgrvtx13starlem1  48425  gpg5nbgrvtx13starlem3  48427  uzlidlring  48589  ply1mulgsumlem2  48741  fllog2  48922  dignn0flhalflem1  48969