Theorem sylibd 238

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3imtr3d  292  ceqsalt  3471  sbceqalOLD  3794  csbiebt  3873  rspcsbela  4383  sneqrg  4785  preq1b  4792  csbexg  5255  elrnrexdm  7022  isoselem  7269  funeldmb  7287  riotass2  7325  ordzsl  7760  oaword2  8456  oaordex  8461  omword1  8476  om00  8478  omeulem2  8486  oen0  8489  oeeui  8505  nnaordex  8541  php3  9078  php3OLD  9090  onomeneqOLD  9095  frfi  9154  infglb  9348  suc11reg  9477  cardne  9823  cardsdomel  9832  carduni  9839  acndom  9909  alephinit  9953  cfflb  10117  cfslb2n  10126  fin23lem28  10198  isf34lem6  10238  fin1a2lem9  10266  axcc3  10296  winalim2  10554  inar1  10633  rankcf  10635  addclprlem2  10875  mulclprlem  10877  ltexprlem7  10900  prlem936  10905  reclem4pr  10908  sqgt0sr  10964  ltord2  11606  leord2  11607  eqord2  11608  mulgt1  11936  mulge0b  11947  lt2halves  12310  addltmul  12311  ltsubnn0  12386  nzadd  12470  zextlt  12496  recnz  12497  zeo  12508  peano5uzi  12511  uzm1  12718  irradd  12815  irrmul  12816  xltneg  13053  xleadd1  13091  xmulasslem  13121  xlemul1a  13124  xlemul1  13126  fznuz  13440  uznfz  13441  axdc4uzlem  13805  facndiv  14104  hashvnfin  14176  hashgt12el  14238  hashgt12el2  14239  hashf1  14272  ccatalpha  14398  swrdccatin2  14541  swrdccatin2d  14556  rennim  15050  cau3lem  15166  caubnd2  15169  o1lo1  15346  climrlim2  15356  climshft  15385  subcn2  15404  mulcn2  15405  rlimo1  15426  o1dif  15439  isercoll  15479  caucvgrlem  15484  serf0  15492  cvgrat  15695  efieq1re  16008  moddvds  16074  dvdsssfz1  16127  smuval2  16289  nn0seqcvgd  16373  algcvgblem  16380  eucalglt  16388  lcmgcdlem  16409  rpmul  16462  divgcdcoprm0  16468  isprm6  16517  rpexp  16525  eulerthlem2  16581  prmdiv  16584  pcprendvds2  16640  pcz  16680  pcprmpw  16682  pcadd2  16689  pcfac  16698  expnprm  16701  ramlb  16818  firest  17241  joineu  18198  meeteu  18212  latjlej1  18269  latjlej2  18270  latmlem1  18285  latmlem2  18286  lubun  18331  acsmapd  18370  imasgrp2  18787  issubg4  18871  psgnunilem4  19202  oddvdsnn0  19249  odmulgeq  19261  subgpgp  19299  odcau  19306  lsmlub  19366  frgpnabllem1  19570  pgpfac1lem2  19774  pgpfac1lem3a  19775  pgpfac1lem3  19776  irredrmul  20045  islmhm2  20407  lsmelval2  20454  lspsnat  20514  znidomb  20876  ip2eq  20965  lsmcss  21004  cnpnei  22522  cncls2  22531  cncls  22532  cnntr  22533  cnt0  22604  isnrm2  22616  comppfsc  22790  kqcldsat  22991  isr0  22995  hmeoopn  23024  hmeocld  23025  trufil  23168  opnsubg  23366  ghmcnp  23373  tgphaus  23375  qustgpopn  23378  tsmsgsum  23397  isngp4  23875  xrhmeo  24216  bndth  24228  cfilres  24567  caubl  24579  ivthlem2  24723  ovolicc2  24793  ismbf3d  24925  itg1ge0a  24983  mbfi1flim  24995  itg2gt0  25032  dvge0  25277  dvcnvrelem1  25288  dvcvx  25291  mdegmullem  25350  ig1peu  25443  plyco  25509  coemulc  25523  dgreq0  25533  dgrlt  25534  plymul0or  25548  plydiveu  25565  quotcan  25576  aalioulem3  25601  ulmcaulem  25660  sincosq3sgn  25764  sincosq4sgn  25765  sineq0  25787  logrec  26020  xrlimcnp  26225  cxploglim  26234  lgamgulmlem1  26285  mumul  26437  chtub  26467  perfect1  26483  dchrelbas3  26493  lgsdir2lem4  26583  lgsne0  26590  lgsquad2lem2  26640  2sqlem8a  26680  2sqblem  26686  nogt01o  26951  axcontlem2  27623  elntg2  27643  redwlklem  28328  redwlk  28329  crctcshwlkn0lem3  28466  crctcshwlkn0lem5  28468  clwwlkext2edg  28709  wwlksubclwwlk  28711  frgrwopregasn  28969  frgrwopregbsn  28970  blocnilem  29455  ip2eqi  29507  ubthlem2  29522  hial0  29753  hial02  29754  hial2eq  29757  h1datomi  30232  sumspansn  30300  lnopcnbd  30687  riesz4i  30714  bra11  30759  pjss2coi  30815  pjnormssi  30819  pjorthcoi  30820  pjclem4a  30849  pj3lem1  30857  pj3cor1i  30860  hst1h  30878  stm1i  30894  strlem1  30901  golem2  30923  mdbr2  30947  dmdbr5  30959  mdsl2i  30973  atexch  31032  atcvatlem  31036  chirredlem1  31041  cdjreui  31083  cdj1i  31084  cdj3lem1  31085  xraddge02  31366  submarchi  31727  isarchiofld  31816  esumcvg  32352  bnj1468  33125  loop1cycl  33398  erdsze2lem2  33465  sltlpss  34197  sltadd2im  34249  btwnexch  34466  btwncolinear2  34511  btwncolinear3  34512  btwncolinear4  34513  btwncolinear5  34514  btwncolinear6  34515  nn0prpw  34651  cldbnd  34654  onsuct0  34769  onint1  34777  bj-ceqsalt0  35207  bj-ceqsalt1  35208  bj-inftyexpiinj  35536  bj-bary1lem1  35638  bj-bary1  35639  relowlssretop  35690  isinf2  35732  ltflcei  35921  tan2h  35925  poimirlem26  35959  poimirlem31  35964  ftc1anclem6  36011  dvasin  36017  dvacos  36018  fdc  36059  caushft  36075  heibor1lem  36123  bfplem2  36137  rrncmslem  36146  rngosn3  36238  mpobi123f  36476  riotasv3d  37278  lsatcv1  37366  lub0N  37507  glb0N  37511  oplecon3b  37518  cmtbr4N  37573  cvrnbtwn2  37593  atnlt  37631  atlatle  37638  cvlsupr2  37661  cvrexchlem  37738  cvratlem  37740  atcvrj0  37747  cvrat4  37762  cvrat42  37763  4noncolr3  37772  ps-1  37796  llnnlt  37842  lplnnlt  37884  lvolnltN  37937  dalempnes  37970  dalemqnet  37971  dalem-cly  37990  dalem44  38035  pmaple  38080  cdlemblem  38112  paddss  38164  2polcon4bN  38237  ltrneq2  38467  cdlemc3  38512  cdleme11h  38585  cdleme16b  38598  cdlemednpq  38618  tendospcanN  39342  dihmeetlem13N  39638  mapdordlem2  39956  mapdn0  39988  isdomn4  40480  ccatcan2d  40522  ctbnfien  40953  rmxypairf1o  41047  monotoddzzfi  41078  oddcomabszz  41080  acongtr  41114  frege124d  41742  expgrowth  42326  sbcbi  42532  limsupmnflem  43649  funressnfv  44955  funfocofob  44988  2elfz2melfz  45228  iccpartnel  45308  requad2  45493  uzlidlring  45905  ply1mulgsumlem2  46146  fllog2  46332  dignn0flhalflem1  46379