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  3867  rspcsbela  4379  sneqrg  4783  preq1b  4790  csbexg  5245  elrnrexdm  7035  isoselem  7289  funeldmb  7307  riotass2  7347  ordzsl  7789  resf1extb  7878  oaword2  8481  oaordex  8486  omword1  8501  om00  8503  omeulem2  8511  oen0  8515  oeeui  8531  nnaordex  8567  php3  9136  frfi  9188  infglb  9397  suc11reg  9531  cardne  9880  cardsdomel  9889  carduni  9896  acndom  9964  alephinit  10008  cfflb  10172  cfslb2n  10181  fin23lem28  10253  isf34lem6  10293  fin1a2lem9  10321  axcc3  10351  winalim2  10610  inar1  10689  rankcf  10691  addclprlem2  10931  mulclprlem  10933  ltexprlem7  10956  prlem936  10961  reclem4pr  10964  sqgt0sr  11020  ltord2  11670  leord2  11671  eqord2  11672  mulgt1OLD  12005  mulge0b  12017  lt2halves  12403  addltmul  12404  ltsubnn0  12479  nzadd  12566  zextlt  12594  recnz  12595  zeo  12606  peano5uzi  12609  uzm1  12813  irradd  12914  irrmul  12915  xltneg  13160  xleadd1  13198  xmulasslem  13228  xlemul1a  13231  xlemul1  13233  fznuz  13554  uznfz  13555  axdc4uzlem  13936  facndiv  14241  hashvnfin  14313  hashgt12el  14375  hashgt12el2  14376  hashf1  14410  ccatalpha  14547  swrdccatin2  14682  swrdccatin2d  14697  rennim  15192  cau3lem  15308  caubnd2  15311  o1lo1  15490  climrlim2  15500  climshft  15529  subcn2  15548  mulcn2  15549  rlimo1  15570  o1dif  15583  isercoll  15621  caucvgrlem  15626  serf0  15634  cvgrat  15839  efieq1re  16157  moddvds  16223  dvdsssfz1  16278  smuval2  16442  nn0seqcvgd  16530  algcvgblem  16537  eucalglt  16545  lcmgcdlem  16566  rpmul  16619  divgcdcoprm0  16625  isprm6  16675  rpexp  16683  eulerthlem2  16743  prmdiv  16746  pcprendvds2  16803  pcz  16843  pcprmpw  16845  pcadd2  16852  pcfac  16861  expnprm  16864  ramlb  16981  firest  17386  joineu  18337  meeteu  18351  latjlej1  18410  latjlej2  18411  latmlem1  18426  latmlem2  18427  lubun  18472  acsmapd  18511  imasgrp2  19022  issubg4  19112  psgnunilem4  19463  oddvdsnn0  19510  odmulgeq  19523  subgpgp  19563  odcau  19570  lsmlub  19630  frgpnabllem1  19839  pgpfac1lem2  20043  pgpfac1lem3a  20044  pgpfac1lem3  20045  irredrmul  20398  isdomn4  20684  islmhm2  21025  lsmelval2  21072  lspsnat  21135  znidomb  21551  ip2eq  21643  lsmcss  21682  cnpnei  23239  cncls2  23248  cncls  23249  cnntr  23250  cnt0  23321  isnrm2  23333  comppfsc  23507  kqcldsat  23708  isr0  23712  hmeoopn  23741  hmeocld  23742  trufil  23885  opnsubg  24083  ghmcnp  24090  tgphaus  24092  qustgpopn  24095  tsmsgsum  24114  isngp4  24587  xrhmeo  24923  bndth  24935  cfilres  25273  caubl  25285  ivthlem2  25429  ovolicc2  25499  ismbf3d  25631  itg1ge0a  25688  mbfi1flim  25700  itg2gt0  25737  dvge0  25983  dvcnvrelem1  25994  dvcvx  25997  mdegmullem  26053  ig1peu  26150  plyco  26216  coemulc  26230  dgreq0  26240  dgrlt  26241  plymul0or  26257  plydiveu  26275  quotcan  26286  aalioulem3  26311  ulmcaulem  26372  sincosq3sgn  26477  sincosq4sgn  26478  sineq0  26501  logrec  26740  xrlimcnp  26945  cxploglim  26955  lgamgulmlem1  27006  mumul  27158  chtub  27189  perfect1  27205  dchrelbas3  27215  lgsdir2lem4  27305  lgsne0  27312  lgsquad2lem2  27362  2sqlem8a  27402  2sqblem  27408  nogt01o  27674  ltslpss  27914  ltadds2im  27992  ltnegs  28051  z12bday  28491  axcontlem2  29048  elntg2  29068  redwlklem  29753  redwlk  29754  crctcshwlkn0lem3  29895  crctcshwlkn0lem5  29897  clwwlkext2edg  30141  wwlksubclwwlk  30143  frgrwopregasn  30401  frgrwopregbsn  30402  blocnilem  30890  ip2eqi  30942  ubthlem2  30957  hial0  31188  hial02  31189  hial2eq  31192  h1datomi  31667  sumspansn  31735  lnopcnbd  32122  riesz4i  32149  bra11  32194  pjss2coi  32250  pjnormssi  32254  pjorthcoi  32255  pjclem4a  32284  pj3lem1  32292  pj3cor1i  32295  hst1h  32313  stm1i  32329  strlem1  32336  golem2  32358  mdbr2  32382  dmdbr5  32394  mdsl2i  32408  atexch  32467  atcvatlem  32471  chirredlem1  32476  cdjreui  32518  cdj1i  32519  cdj3lem1  32520  xraddge02  32845  submarchi  33262  isarchiofld  33275  esumcvg  34246  bnj1468  35004  loop1cycl  35335  erdsze2lem2  35402  btwnexch  36223  btwncolinear2  36268  btwncolinear3  36269  btwncolinear4  36270  btwncolinear5  36271  btwncolinear6  36272  nn0prpw  36521  cldbnd  36524  onsuct0  36639  onint1  36647  bj-ceqsalt0  37207  bj-ceqsalt1  37208  bj-inftyexpiinj  37539  bj-bary1lem1  37641  bj-bary1  37642  relowlssretop  37693  isinf2  37735  ltflcei  37943  tan2h  37947  poimirlem26  37981  poimirlem31  37986  ftc1anclem6  38033  dvasin  38039  dvacos  38040  fdc  38080  caushft  38096  heibor1lem  38144  bfplem2  38158  rrncmslem  38167  rngosn3  38259  mpobi123f  38497  riotasv3d  39420  lsatcv1  39508  lub0N  39649  glb0N  39653  oplecon3b  39660  cmtbr4N  39715  cvrnbtwn2  39735  atnlt  39773  atlatle  39780  cvlsupr2  39803  cvrexchlem  39879  cvratlem  39881  atcvrj0  39888  cvrat4  39903  cvrat42  39904  4noncolr3  39913  ps-1  39937  llnnlt  39983  lplnnlt  40025  lvolnltN  40078  dalempnes  40111  dalemqnet  40112  dalem-cly  40131  dalem44  40176  pmaple  40221  cdlemblem  40253  paddss  40305  2polcon4bN  40378  ltrneq2  40608  cdlemc3  40653  cdleme11h  40726  cdleme16b  40739  cdlemednpq  40759  tendospcanN  41483  dihmeetlem13N  41779  mapdordlem2  42097  mapdn0  42129  rspcsbnea  42584  ccatcan2d  42704  ctbnfien  43264  rmxypairf1o  43357  monotoddzzfi  43388  oddcomabszz  43390  acongtr  43424  onsupnmax  43674  onsupsucismax  43725  frege124d  44206  expgrowth  44780  sbcbi  44984  limsupmnflem  46166  funressnfv  47503  funfocofob  47538  2elfz2melfz  47778  iccpartnel  47910  requad2  48111  grlictr  48503  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem3  48561  uzlidlring  48723  ply1mulgsumlem2  48875  fllog2  49056  dignn0flhalflem1  49103