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  3877  rspcsbela  4386  sneqrg  4789  preq1b  4796  csbexg  5246  elrnrexdm  7017  isoselem  7270  funeldmb  7288  riotass2  7328  ordzsl  7770  resf1extb  7859  oaword2  8463  oaordex  8468  omword1  8483  om00  8485  omeulem2  8493  oen0  8496  oeeui  8512  nnaordex  8548  php3  9113  frfi  9164  infglb  9370  suc11reg  9504  cardne  9850  cardsdomel  9859  carduni  9866  acndom  9934  alephinit  9978  cfflb  10142  cfslb2n  10151  fin23lem28  10223  isf34lem6  10263  fin1a2lem9  10291  axcc3  10321  winalim2  10579  inar1  10658  rankcf  10660  addclprlem2  10900  mulclprlem  10902  ltexprlem7  10925  prlem936  10930  reclem4pr  10933  sqgt0sr  10989  ltord2  11638  leord2  11639  eqord2  11640  mulgt1OLD  11972  mulge0b  11984  lt2halves  12348  addltmul  12349  ltsubnn0  12424  nzadd  12512  zextlt  12539  recnz  12540  zeo  12551  peano5uzi  12554  uzm1  12762  irradd  12863  irrmul  12864  xltneg  13108  xleadd1  13146  xmulasslem  13176  xlemul1a  13179  xlemul1  13181  fznuz  13501  uznfz  13502  axdc4uzlem  13882  facndiv  14187  hashvnfin  14259  hashgt12el  14321  hashgt12el2  14322  hashf1  14356  ccatalpha  14493  swrdccatin2  14628  swrdccatin2d  14643  rennim  15138  cau3lem  15254  caubnd2  15257  o1lo1  15436  climrlim2  15446  climshft  15475  subcn2  15494  mulcn2  15495  rlimo1  15516  o1dif  15529  isercoll  15567  caucvgrlem  15572  serf0  15580  cvgrat  15782  efieq1re  16100  moddvds  16166  dvdsssfz1  16221  smuval2  16385  nn0seqcvgd  16473  algcvgblem  16480  eucalglt  16488  lcmgcdlem  16509  rpmul  16562  divgcdcoprm0  16568  isprm6  16617  rpexp  16625  eulerthlem2  16685  prmdiv  16688  pcprendvds2  16745  pcz  16785  pcprmpw  16787  pcadd2  16794  pcfac  16803  expnprm  16806  ramlb  16923  firest  17328  joineu  18278  meeteu  18292  latjlej1  18351  latjlej2  18352  latmlem1  18367  latmlem2  18368  lubun  18413  acsmapd  18452  imasgrp2  18960  issubg4  19050  psgnunilem4  19402  oddvdsnn0  19449  odmulgeq  19462  subgpgp  19502  odcau  19509  lsmlub  19569  frgpnabllem1  19778  pgpfac1lem2  19982  pgpfac1lem3a  19983  pgpfac1lem3  19984  irredrmul  20338  isdomn4  20624  islmhm2  20965  lsmelval2  21012  lspsnat  21075  znidomb  21491  ip2eq  21583  lsmcss  21622  cnpnei  23172  cncls2  23181  cncls  23182  cnntr  23183  cnt0  23254  isnrm2  23266  comppfsc  23440  kqcldsat  23641  isr0  23645  hmeoopn  23674  hmeocld  23675  trufil  23818  opnsubg  24016  ghmcnp  24023  tgphaus  24025  qustgpopn  24028  tsmsgsum  24047  isngp4  24520  xrhmeo  24864  bndth  24877  cfilres  25216  caubl  25228  ivthlem2  25373  ovolicc2  25443  ismbf3d  25575  itg1ge0a  25632  mbfi1flim  25644  itg2gt0  25681  dvge0  25931  dvcnvrelem1  25942  dvcvx  25945  mdegmullem  26003  ig1peu  26100  plyco  26166  coemulc  26180  dgreq0  26191  dgrlt  26192  plymul0or  26208  plydiveu  26226  quotcan  26237  aalioulem3  26262  ulmcaulem  26323  sincosq3sgn  26429  sincosq4sgn  26430  sineq0  26453  logrec  26693  xrlimcnp  26898  cxploglim  26908  lgamgulmlem1  26959  mumul  27111  chtub  27143  perfect1  27159  dchrelbas3  27169  lgsdir2lem4  27259  lgsne0  27266  lgsquad2lem2  27316  2sqlem8a  27356  2sqblem  27362  nogt01o  27628  sltlpss  27846  sltadd2im  27922  sltneg  27980  axcontlem2  28936  elntg2  28956  redwlklem  29641  redwlk  29642  crctcshwlkn0lem3  29783  crctcshwlkn0lem5  29785  clwwlkext2edg  30026  wwlksubclwwlk  30028  frgrwopregasn  30286  frgrwopregbsn  30287  blocnilem  30774  ip2eqi  30826  ubthlem2  30841  hial0  31072  hial02  31073  hial2eq  31076  h1datomi  31551  sumspansn  31619  lnopcnbd  32006  riesz4i  32033  bra11  32078  pjss2coi  32134  pjnormssi  32138  pjorthcoi  32139  pjclem4a  32168  pj3lem1  32176  pj3cor1i  32179  hst1h  32197  stm1i  32213  strlem1  32220  golem2  32242  mdbr2  32266  dmdbr5  32278  mdsl2i  32292  atexch  32351  atcvatlem  32355  chirredlem1  32360  cdjreui  32402  cdj1i  32403  cdj3lem1  32404  xraddge02  32730  submarchi  33145  isarchiofld  33158  esumcvg  34089  bnj1468  34848  loop1cycl  35149  erdsze2lem2  35216  btwnexch  36038  btwncolinear2  36083  btwncolinear3  36084  btwncolinear4  36085  btwncolinear5  36086  btwncolinear6  36087  nn0prpw  36336  cldbnd  36339  onsuct0  36454  onint1  36462  bj-ceqsalt0  36897  bj-ceqsalt1  36898  bj-inftyexpiinj  37222  bj-bary1lem1  37324  bj-bary1  37325  relowlssretop  37376  isinf2  37418  ltflcei  37627  tan2h  37631  poimirlem26  37665  poimirlem31  37670  ftc1anclem6  37717  dvasin  37723  dvacos  37724  fdc  37764  caushft  37780  heibor1lem  37828  bfplem2  37842  rrncmslem  37851  rngosn3  37943  mpobi123f  38181  riotasv3d  38978  lsatcv1  39066  lub0N  39207  glb0N  39211  oplecon3b  39218  cmtbr4N  39273  cvrnbtwn2  39293  atnlt  39331  atlatle  39338  cvlsupr2  39361  cvrexchlem  39437  cvratlem  39439  atcvrj0  39446  cvrat4  39461  cvrat42  39462  4noncolr3  39471  ps-1  39495  llnnlt  39541  lplnnlt  39583  lvolnltN  39636  dalempnes  39669  dalemqnet  39670  dalem-cly  39689  dalem44  39734  pmaple  39779  cdlemblem  39811  paddss  39863  2polcon4bN  39936  ltrneq2  40166  cdlemc3  40211  cdleme11h  40284  cdleme16b  40297  cdlemednpq  40317  tendospcanN  41041  dihmeetlem13N  41337  mapdordlem2  41655  mapdn0  41687  rspcsbnea  42143  ccatcan2d  42263  ctbnfien  42830  rmxypairf1o  42923  monotoddzzfi  42954  oddcomabszz  42956  acongtr  42990  onsupnmax  43240  onsupsucismax  43291  frege124d  43773  expgrowth  44347  sbcbi  44551  limsupmnflem  45737  funressnfv  47053  funfocofob  47088  2elfz2melfz  47328  iccpartnel  47448  requad2  47633  grlictr  48025  gpg5nbgrvtx13starlem1  48081  gpg5nbgrvtx13starlem3  48083  uzlidlring  48245  ply1mulgsumlem2  48398  fllog2  48579  dignn0flhalflem1  48626