Theorem sylibd 228

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  3imtr3d  281  ceqsalt  3201  sbceqal  3454  csbiebt  3519  rspcsbela  3958  sneqrg  4310  preq1b  4317  csbexg  4720  elrnrexdm  6271  isoselem  6491  riotass2  6537  ordzsl  6937  oaword2  7520  oaordex  7525  omword1  7540  om00  7542  omeulem2  7550  oen0  7553  oeeui  7569  nnaordex  7605  php3  8031  onomeneq  8035  frfi  8090  infglb  8279  suc11reg  8399  cardne  8674  cardsdomel  8683  carduni  8690  acndom  8757  alephinit  8801  cfflb  8964  cfslb2n  8973  fin23lem28  9045  isf34lem6  9085  fin1a2lem9  9113  axcc3  9143  winalim2  9397  inar1  9476  rankcf  9478  addclprlem2  9718  mulclprlem  9720  ltexprlem7  9743  prlem936  9748  reclem4pr  9751  sqgt0sr  9806  ltord2  10436  leord2  10437  eqord2  10438  mulgt1  10761  mulge0b  10772  fiminre  10851  lt2halves  11144  addltmul  11145  ltsubnn0  11221  nzadd  11302  zextlt  11327  recnz  11328  zeo  11339  peano5uzi  11342  uzm1  11594  irradd  11688  irrmul  11689  xltneg  11922  xleadd1  11957  xmulasslem  11987  xlemul1a  11990  xlemul1  11992  fznuz  12291  uznfz  12292  axdc4uzlem  12644  facndiv  12937  hashvnfin  13012  hashgt12el  13070  hashgt12el2  13071  hashf1  13098  ccatalpha  13228  swrdccatin2  13338  swrdccatin2d  13351  swrdccatin12d  13352  rennim  13827  cau3lem  13942  caubnd2  13945  o1lo1  14116  climrlim2  14126  climshft  14155  subcn2  14173  mulcn2  14174  rlimo1  14195  o1dif  14208  isercoll  14246  caucvgrlem  14251  serf0  14259  cvgrat  14454  efieq1re  14768  moddvds  14829  dvdsssfz1  14878  smuval2  15042  nn0seqcvgd  15121  algcvgblem  15128  eucalglt  15136  lcmgcdlem  15157  coprmdvdsOLD  15205  rpmul  15211  divgcdcoprm0  15217  isprm6  15264  rpexp  15270  eulerthlem2  15325  prmdiv  15328  pcprendvds2  15384  pcz  15423  pcprmpw  15425  pcadd2  15432  pcfac  15441  expnprm  15444  ramlb  15561  firest  15916  joineu  16833  meeteu  16847  latjlej1  16888  latjlej2  16889  latmlem1  16904  latmlem2  16905  lubun  16946  acsmapd  17001  imasgrp2  17353  issubg4  17436  psgnunilem4  17740  oddvdsnn0  17786  odmulgeq  17797  subgpgp  17835  odcau  17842  lsmlub  17901  frgpnabllem1  18099  pgpfac1lem2  18297  pgpfac1lem3a  18298  pgpfac1lem3  18299  irredrmul  18530  islmhm2  18859  lsmelval2  18906  lspsnat  18966  znidomb  19729  ip2eq  19817  lsmcss  19855  cnpnei  20878  cncls2  20887  cncls  20888  cnntr  20889  cnt0  20960  isnrm2  20972  comppfsc  21145  kqcldsat  21346  isr0  21350  hmeoopn  21379  hmeocld  21380  trufil  21524  opnsubg  21721  ghmcnp  21728  tgphaus  21730  qustgpopn  21733  tsmsgsum  21752  isngp4  22226  xrhmeo  22553  bndth  22565  cfilres  22902  caubl  22914  ivthlem2  23028  ovolicc2  23097  ismbf3d  23227  itg1ge0a  23284  mbfi1flim  23296  itg2gt0  23333  dvge0  23573  dvcnvrelem1  23584  dvcvx  23587  mdegmullem  23642  ig1peu  23735  plyco  23801  coemulc  23815  dgreq0  23825  dgrlt  23826  plymul0or  23840  plydiveu  23857  quotcan  23868  aalioulem3  23893  ulmcaulem  23952  sincosq3sgn  24056  sincosq4sgn  24057  sineq0  24077  logrec  24301  xrlimcnp  24495  cxploglim  24504  lgamgulmlem1  24555  mumul  24707  chtub  24737  perfect1  24753  dchrelbas3  24763  lgsdir2lem4  24853  lgsne0  24860  lgsquad2lem2  24910  2sqlem8a  24950  2sqblem  24956  axcontlem2  25645  cusgrarn  25988  redwlk  26136  wlkdvspth  26138  wlkiswwlk1  26218  wlklniswwlkn1  26227  clwwlkext2edg  26330  wwlksubclwwlk  26332  clwlkf1clwwlklem  26376  frgrawopreg1  26577  frgrawopreg2  26578  extwwlkfablem2  26605  blocnilem  27043  ip2eqi  27096  ubthlem2  27111  hial0  27343  hial02  27344  hial2eq  27347  h1datomi  27824  sumspansn  27892  lnopcnbd  28279  riesz4i  28306  bra11  28351  pjss2coi  28407  pjnormssi  28411  pjorthcoi  28412  pjclem4a  28441  pj3lem1  28449  pj3cor1i  28452  hst1h  28470  stm1i  28486  strlem1  28493  golem2  28515  mdbr2  28539  dmdbr5  28551  mdsl2i  28565  atexch  28624  atcvatlem  28628  chirredlem1  28633  cdjreui  28675  cdj1i  28676  cdj3lem1  28677  xraddge02  28911  submarchi  29071  isarchiofld  29148  esumcvg  29475  bnj1468  30170  erdsze2lem2  30440  btwnexch  31302  btwncolinear2  31347  btwncolinear3  31348  btwncolinear4  31349  btwncolinear5  31350  btwncolinear6  31351  nn0prpw  31488  cldbnd  31491  onsuct0  31610  onint1  31618  bj-ceqsalt0  32067  bj-ceqsalt1  32068  bj-inftyexpiinj  32273  bj-bary1lem1  32338  bj-bary1  32339  relowlssretop  32387  ltflcei  32567  tan2h  32571  poimirlem26  32605  poimirlem31  32610  ftc1anclem6  32660  dvasin  32666  dvacos  32667  fdc  32711  caushft  32727  heibor1lem  32778  bfplem2  32792  rrncmslem  32801  rngosn3  32893  mpt2bi123f  33141  riotasv3d  33264  lsatcv1  33353  lub0N  33494  glb0N  33498  oplecon3b  33505  cmtbr4N  33560  cvrnbtwn2  33580  atnlt  33618  atlatle  33625  cvlsupr2  33648  cvrexchlem  33723  cvratlem  33725  atcvrj0  33732  cvrat4  33747  cvrat42  33748  4noncolr3  33757  ps-1  33781  llnnlt  33827  lplnnlt  33869  lvolnltN  33922  dalempnes  33955  dalemqnet  33956  dalem-cly  33975  dalem44  34020  pmaple  34065  cdlemblem  34097  paddss  34149  2polcon4bN  34222  ltrneq2  34452  cdlemc3  34498  cdleme11h  34571  cdleme16b  34584  cdlemednpq  34604  tendospcanN  35330  dihmeetlem13N  35626  mapdordlem2  35944  mapdn0  35976  ctbnfien  36400  rmxypairf1o  36494  monotoddzzfi  36525  oddcomabszz  36527  acongtr  36563  frege124d  37072  expgrowth  37556  sbcbi  37770  csbeq2gOLD  37786  funressnfv  39857  iccpartnel  39976  2elfz2melfz  40355  red1wlklem  40880  red1wlk  40881  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem5  41017  clwwlksext2edg  41230  wwlksubclwwlks  41232  clwlksf1clwwlklem  41275  frgrwopreg1  41487  frgrwopreg2  41488  av-extwwlkfablem2  41510  uzlidlring  41719  ply1mulgsumlem2  41969  fllog2  42160  dignn0flhalflem1  42207