Theorem sylibd 242

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3imtr3d  296  csbiebt  3884  rspcsbela  4395  sneqrg  4800  preq1b  4807  csbexg  5265  elrnrexdm  7074  isoselem  7329  funeldmb  7347  riotass2  7387  ordzsl  7829  resf1extb  7919  oaword2  8526  oaordex  8531  omword1  8546  om00  8548  omeulem2  8556  oen0  8560  oeeui  8576  nnaordex  8612  php3  9181  frfi  9233  infglb  9439  suc11reg  9576  cardne  9939  cardsdomel  9948  carduni  9955  acndom  10023  alephinit  10067  cfflb  10231  cfslb2n  10240  fin23lem28  10312  isf34lem6  10352  fin1a2lem9  10380  axcc3  10410  winalim2  10669  inar1  10748  rankcf  10750  addclprlem2  10990  mulclprlem  10992  ltexprlem7  11015  prlem936  11020  reclem4pr  11023  sqgt0sr  11079  ltord2  11731  leord2  11732  eqord2  11733  mulge0b  12076  lt2halves  12470  addltmul  12471  ltsubnn0  12546  nzadd  12633  zextlt  12661  recnz  12662  zeo  12673  peano5uzi  12676  uzm1  12887  irradd  12988  irrmul  12989  xltneg  13234  xleadd1  13272  xmulasslem  13302  xlemul1a  13305  xlemul1  13307  fznuz  13628  uznfz  13629  axdc4uzlem  14010  facndiv  14315  hashvnfin  14387  hashgt12el  14449  hashgt12el2  14450  hashf1  14484  ccatalpha  14621  swrdccatin2  14756  swrdccatin2d  14771  rennim  15280  cau3lem  15396  caubnd2  15399  o1lo1  15578  climrlim2  15588  climshft  15617  subcn2  15636  mulcn2  15637  rlimo1  15658  o1dif  15671  isercoll  15709  caucvgrlem  15714  serf0  15722  cvgrat  15927  efieq1re  16245  moddvds  16311  dvdsssfz1  16366  smuval2  16530  nn0seqcvgd  16618  algcvgblem  16625  eucalglt  16633  lcmgcdlem  16654  rpmul  16707  divgcdcoprm0  16713  isprm6  16763  rpexp  16771  eulerthlem2  16831  prmdiv  16834  pcprendvds2  16891  pcz  16931  pcprmpw  16933  pcadd2  16940  pcfac  16949  expnprm  16952  ramlb  17069  firest  17475  joineu  18426  meeteu  18440  latjlej1  18499  latjlej2  18500  latmlem1  18515  latmlem2  18516  lubun  18561  acsmapd  18600  imasgrp2  19112  issubg4  19203  psgnunilem4  19558  oddvdsnn0  19605  odmulgeq  19618  subgpgp  19658  odcau  19665  lsmlub  19725  frgpnabllem1  19934  pgpfac1lem2  20138  pgpfac1lem3a  20139  pgpfac1lem3  20140  irredrmul  20500  isdomn4  20791  islmhm2  21128  lsmelval2  21175  lspsnat  21238  znidomb  21671  ip2eq  21763  lsmcss  21802  cnpnei  23382  cncls2  23391  cncls  23392  cnntr  23393  cnt0  23464  isnrm2  23476  comppfsc  23650  kqcldsat  23851  isr0  23855  hmeoopn  23884  hmeocld  23885  trufil  24028  opnsubg  24226  ghmcnp  24233  tgphaus  24235  qustgpopn  24238  tsmsgsum  24257  isngp4  24730  xrhmeo  25066  bndth  25078  cfilres  25416  caubl  25428  ivthlem2  25572  ovolicc2  25642  ismbf3d  25774  itg1ge0a  25831  mbfi1flim  25843  itg2gt0  25880  dvge0  26126  dvcnvrelem1  26137  dvcvx  26140  mdegmullem  26196  ig1peu  26293  plyco  26359  coemulc  26373  dgreq0  26383  dgrlt  26384  plymul0or  26400  plydiveu  26420  quotcan  26431  aalioulem3  26456  ulmcaulem  26515  sincosq3sgn  26623  sincosq4sgn  26624  sineq0  26647  logrec  26886  xrlimcnp  27091  cxploglim  27100  lgamgulmlem1  27151  mumul  27303  chtub  27334  perfect1  27350  dchrelbas3  27360  lgsdir2lem4  27450  lgsne0  27457  lgsquad2lem2  27507  2sqlem8a  27547  2sqblem  27553  nogt01o  27818  ltslpss  28059  ltadds2im  28137  ltnegs  28196  z12bday  28636  axcontlem2  29224  elntg2  29244  redwlklem  29928  redwlk  29929  crctcshwlkn0lem3  30070  crctcshwlkn0lem5  30072  clwwlkext2edg  30316  wwlksubclwwlk  30318  frgrwopregasn  30576  frgrwopregbsn  30577  blocnilem  31065  ip2eqi  31117  ubthlem2  31132  hial0  31363  hial02  31364  hial2eq  31367  h1datomi  31842  sumspansn  31910  lnopcnbd  32297  riesz4i  32324  bra11  32369  pjss2coi  32425  pjnormssi  32429  pjorthcoi  32430  pjclem4a  32459  pj3lem1  32467  pj3cor1i  32470  hst1h  32488  stm1i  32504  strlem1  32511  golem2  32533  mdbr2  32557  dmdbr5  32569  mdsl2i  32583  atexch  32642  atcvatlem  32646  chirredlem1  32651  cdjreui  32693  cdj1i  32694  cdj3lem1  32695  xraddge02  33014  submarchi  33419  isarchiofld  33432  esumcvg  34393  bnj1468  35151  loop1cycl  35500  erdsze2lem2  35567  btwnexch  36388  btwncolinear2  36433  btwncolinear3  36434  btwncolinear4  36435  btwncolinear5  36436  btwncolinear6  36437  nn0prpw  36696  cldbnd  36699  onsuct0  36814  onint1  36822  bj-ceqsalt0  37381  bj-ceqsalt1  37382  bj-inftyexpiinj  37713  bj-bary1lem1  37815  bj-bary1  37816  relowlssretop  37869  isinf2  37911  ltflcei  38119  tan2h  38123  poimirlem26  38157  poimirlem31  38162  ftc1anclem6  38209  dvasin  38215  dvacos  38216  fdc  38256  caushft  38272  heibor1lem  38320  bfplem2  38334  rrncmslem  38343  rngosn3  38435  mpobi123f  38673  riotasv3d  39596  lsatcv1  39684  lub0N  39825  glb0N  39829  oplecon3b  39836  cmtbr4N  39891  cvrnbtwn2  39911  atnlt  39949  atlatle  39956  cvlsupr2  39979  cvrexchlem  40055  cvratlem  40057  atcvrj0  40064  cvrat4  40079  cvrat42  40080  4noncolr3  40089  ps-1  40113  llnnlt  40159  lplnnlt  40201  lvolnltN  40254  dalempnes  40287  dalemqnet  40288  dalem-cly  40307  dalem44  40352  pmaple  40397  cdlemblem  40429  paddss  40481  2polcon4bN  40554  ltrneq2  40784  cdlemc3  40829  cdleme11h  40902  cdleme16b  40915  cdlemednpq  40935  tendospcanN  41659  dihmeetlem13N  41955  mapdordlem2  42273  mapdn0  42305  rspcsbnea  42760  ccatcan2d  42879  ctbnfien  43407  rmxypairf1o  43500  monotoddzzfi  43531  oddcomabszz  43533  acongtr  43567  onsupnmax  43817  onsupsucismax  43868  frege124d  44349  expgrowth  44909  sbcbi  45113  limsupmnflem  46292  funressnfv  47635  funfocofob  47670  2elfz2melfz  47910  iccpartnel  48042  requad2  48243  grlictr  48635  gpg5nbgrvtx13starlem1  48691  gpg5nbgrvtx13starlem3  48693  uzlidlring  48855  ply1mulgsumlem2  49018  fllog2  49199  dignn0flhalflem1  49246