Theorem sylibd 230

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

Syntax hints:   → wi 4   ↔ wb 197

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 198

This theorem is referenced by:  3imtr3d  284  ceqsalt  3422  sbceqal  3685  csbiebt  3748  rspcsbela  4204  sneqrg  4558  preq1b  4565  csbexg  4987  elrnrexdm  6585  isoselem  6815  riotass2  6862  ordzsl  7275  oaword2  7870  oaordex  7875  omword1  7890  om00  7892  omeulem2  7900  oen0  7903  oeeui  7919  nnaordex  7955  php3  8385  onomeneq  8389  frfi  8444  infglb  8635  suc11reg  8763  cardne  9074  cardsdomel  9083  carduni  9090  acndom  9157  alephinit  9201  cfflb  9366  cfslb2n  9375  fin23lem28  9447  isf34lem6  9487  fin1a2lem9  9515  axcc3  9545  winalim2  9803  inar1  9882  rankcf  9884  addclprlem2  10124  mulclprlem  10126  ltexprlem7  10149  prlem936  10154  reclem4pr  10157  sqgt0sr  10212  ltord2  10842  leord2  10843  eqord2  10844  mulgt1  11167  mulge0b  11178  fiminre  11257  lt2halves  11534  addltmul  11535  ltsubnn0  11610  nzadd  11691  zextlt  11717  recnz  11718  zeo  11729  peano5uzi  11732  uzm1  11936  irradd  12031  irrmul  12032  xltneg  12266  xleadd1  12303  xmulasslem  12333  xlemul1a  12336  xlemul1  12338  fznuz  12645  uznfz  12646  axdc4uzlem  13006  facndiv  13295  hashvnfin  13369  hashgt12el  13427  hashgt12el2  13428  hashf1  13458  ccatalpha  13590  swrdccatin2  13711  swrdccatin2d  13724  swrdccatin12d  13725  rennim  14202  cau3lem  14317  caubnd2  14320  o1lo1  14491  climrlim2  14501  climshft  14530  subcn2  14548  mulcn2  14549  rlimo1  14570  o1dif  14583  isercoll  14621  caucvgrlem  14626  serf0  14634  cvgrat  14836  efieq1re  15149  moddvds  15214  dvdsssfz1  15263  smuval2  15423  nn0seqcvgd  15502  algcvgblem  15509  eucalglt  15517  lcmgcdlem  15538  rpmul  15591  divgcdcoprm0  15597  isprm6  15643  rpexp  15649  eulerthlem2  15704  prmdiv  15707  pcprendvds2  15763  pcz  15802  pcprmpw  15804  pcadd2  15811  pcfac  15820  expnprm  15823  ramlb  15940  firest  16298  joineu  17215  meeteu  17229  latjlej1  17270  latjlej2  17271  latmlem1  17286  latmlem2  17287  lubun  17328  acsmapd  17383  imasgrp2  17735  issubg4  17815  psgnunilem4  18118  oddvdsnn0  18164  odmulgeq  18175  subgpgp  18213  odcau  18220  lsmlub  18279  frgpnabllem1  18477  pgpfac1lem2  18676  pgpfac1lem3a  18677  pgpfac1lem3  18678  irredrmul  18909  islmhm2  19245  lsmelval2  19292  lspsnat  19353  znidomb  20117  ip2eq  20208  lsmcss  20246  cnpnei  21282  cncls2  21291  cncls  21292  cnntr  21293  cnt0  21364  isnrm2  21376  comppfsc  21549  kqcldsat  21750  isr0  21754  hmeoopn  21783  hmeocld  21784  trufil  21927  opnsubg  22124  ghmcnp  22131  tgphaus  22133  qustgpopn  22136  tsmsgsum  22155  isngp4  22629  xrhmeo  22958  bndth  22970  cfilres  23306  caubl  23318  ivthlem2  23433  ovolicc2  23503  ismbf3d  23635  itg1ge0a  23692  mbfi1flim  23704  itg2gt0  23741  dvge0  23983  dvcnvrelem1  23994  dvcvx  23997  mdegmullem  24052  ig1peu  24145  plyco  24211  coemulc  24225  dgreq0  24235  dgrlt  24236  plymul0or  24250  plydiveu  24267  quotcan  24278  aalioulem3  24303  ulmcaulem  24362  sincosq3sgn  24467  sincosq4sgn  24468  sineq0  24488  logrec  24715  xrlimcnp  24909  cxploglim  24918  lgamgulmlem1  24969  mumul  25121  chtub  25151  perfect1  25167  dchrelbas3  25177  lgsdir2lem4  25267  lgsne0  25274  lgsquad2lem2  25324  2sqlem8a  25364  2sqblem  25370  axcontlem2  26059  redwlklem  26796  redwlk  26797  crctcshwlkn0lem3  26933  crctcshwlkn0lem5  26935  clwwlkext2edg  27206  wwlksubclwwlk  27209  clwlksf1clwwlklemOLD  27242  frgrwopregasn  27491  frgrwopregbsn  27492  blocnilem  27987  ip2eqi  28040  ubthlem2  28055  hial0  28287  hial02  28288  hial2eq  28291  h1datomi  28768  sumspansn  28836  lnopcnbd  29223  riesz4i  29250  bra11  29295  pjss2coi  29351  pjnormssi  29355  pjorthcoi  29356  pjclem4a  29385  pj3lem1  29393  pj3cor1i  29396  hst1h  29414  stm1i  29430  strlem1  29437  golem2  29459  mdbr2  29483  dmdbr5  29495  mdsl2i  29509  atexch  29568  atcvatlem  29572  chirredlem1  29577  cdjreui  29619  cdj1i  29620  cdj3lem1  29621  xraddge02  29848  submarchi  30065  isarchiofld  30142  esumcvg  30473  bnj1468  31239  erdsze2lem2  31509  funeldmb  31983  btwnexch  32453  btwncolinear2  32498  btwncolinear3  32499  btwncolinear4  32500  btwncolinear5  32501  btwncolinear6  32502  nn0prpw  32639  cldbnd  32642  onsuct0  32757  onint1  32765  bj-ceqsalt0  33181  bj-ceqsalt1  33182  bj-inftyexpiinj  33413  bj-bary1lem1  33478  bj-bary1  33479  relowlssretop  33527  ltflcei  33710  tan2h  33714  poimirlem26  33748  poimirlem31  33753  ftc1anclem6  33802  dvasin  33808  dvacos  33809  fdc  33852  caushft  33868  heibor1lem  33919  bfplem2  33933  rrncmslem  33942  rngosn3  34034  mpt2bi123f  34281  riotasv3d  34739  lsatcv1  34828  lub0N  34969  glb0N  34973  oplecon3b  34980  cmtbr4N  35035  cvrnbtwn2  35055  atnlt  35093  atlatle  35100  cvlsupr2  35123  cvrexchlem  35199  cvratlem  35201  atcvrj0  35208  cvrat4  35223  cvrat42  35224  4noncolr3  35233  ps-1  35257  llnnlt  35303  lplnnlt  35345  lvolnltN  35398  dalempnes  35431  dalemqnet  35432  dalem-cly  35451  dalem44  35496  pmaple  35541  cdlemblem  35573  paddss  35625  2polcon4bN  35698  ltrneq2  35928  cdlemc3  35974  cdleme11h  36047  cdleme16b  36060  cdlemednpq  36080  tendospcanN  36804  dihmeetlem13N  37100  mapdordlem2  37418  mapdn0  37450  ctbnfien  37884  rmxypairf1o  37977  monotoddzzfi  38008  oddcomabszz  38010  acongtr  38046  frege124d  38553  expgrowth  39034  sbcbi  39247  csbeq2gOLD  39263  limsupmnflem  40432  funressnfv  41662  2elfz2melfz  41903  iccpartnel  41949  uzlidlring  42497  ply1mulgsumlem2  42743  fllog2  42930  dignn0flhalflem1  42977