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  3891  rspcsbela  4401  sneqrg  4803  preq1b  4810  csbexg  5265  elrnrexdm  7061  isoselem  7316  funeldmb  7334  riotass2  7374  ordzsl  7821  resf1extb  7910  oaword2  8517  oaordex  8522  omword1  8537  om00  8539  omeulem2  8547  oen0  8550  oeeui  8566  nnaordex  8602  php3  9173  frfi  9232  infglb  9442  suc11reg  9572  cardne  9918  cardsdomel  9927  carduni  9934  acndom  10004  alephinit  10048  cfflb  10212  cfslb2n  10221  fin23lem28  10293  isf34lem6  10333  fin1a2lem9  10361  axcc3  10391  winalim2  10649  inar1  10728  rankcf  10730  addclprlem2  10970  mulclprlem  10972  ltexprlem7  10995  prlem936  11000  reclem4pr  11003  sqgt0sr  11059  ltord2  11707  leord2  11708  eqord2  11709  mulgt1OLD  12041  mulge0b  12053  lt2halves  12417  addltmul  12418  ltsubnn0  12493  nzadd  12581  zextlt  12608  recnz  12609  zeo  12620  peano5uzi  12623  uzm1  12831  irradd  12932  irrmul  12933  xltneg  13177  xleadd1  13215  xmulasslem  13245  xlemul1a  13248  xlemul1  13250  fznuz  13570  uznfz  13571  axdc4uzlem  13948  facndiv  14253  hashvnfin  14325  hashgt12el  14387  hashgt12el2  14388  hashf1  14422  ccatalpha  14558  swrdccatin2  14694  swrdccatin2d  14709  rennim  15205  cau3lem  15321  caubnd2  15324  o1lo1  15503  climrlim2  15513  climshft  15542  subcn2  15561  mulcn2  15562  rlimo1  15583  o1dif  15596  isercoll  15634  caucvgrlem  15639  serf0  15647  cvgrat  15849  efieq1re  16167  moddvds  16233  dvdsssfz1  16288  smuval2  16452  nn0seqcvgd  16540  algcvgblem  16547  eucalglt  16555  lcmgcdlem  16576  rpmul  16629  divgcdcoprm0  16635  isprm6  16684  rpexp  16692  eulerthlem2  16752  prmdiv  16755  pcprendvds2  16812  pcz  16852  pcprmpw  16854  pcadd2  16861  pcfac  16870  expnprm  16873  ramlb  16990  firest  17395  joineu  18341  meeteu  18355  latjlej1  18412  latjlej2  18413  latmlem1  18428  latmlem2  18429  lubun  18474  acsmapd  18513  imasgrp2  18987  issubg4  19077  psgnunilem4  19427  oddvdsnn0  19474  odmulgeq  19487  subgpgp  19527  odcau  19534  lsmlub  19594  frgpnabllem1  19803  pgpfac1lem2  20007  pgpfac1lem3a  20008  pgpfac1lem3  20009  irredrmul  20336  isdomn4  20625  islmhm2  20945  lsmelval2  20992  lspsnat  21055  znidomb  21471  ip2eq  21562  lsmcss  21601  cnpnei  23151  cncls2  23160  cncls  23161  cnntr  23162  cnt0  23233  isnrm2  23245  comppfsc  23419  kqcldsat  23620  isr0  23624  hmeoopn  23653  hmeocld  23654  trufil  23797  opnsubg  23995  ghmcnp  24002  tgphaus  24004  qustgpopn  24007  tsmsgsum  24026  isngp4  24500  xrhmeo  24844  bndth  24857  cfilres  25196  caubl  25208  ivthlem2  25353  ovolicc2  25423  ismbf3d  25555  itg1ge0a  25612  mbfi1flim  25624  itg2gt0  25661  dvge0  25911  dvcnvrelem1  25922  dvcvx  25925  mdegmullem  25983  ig1peu  26080  plyco  26146  coemulc  26160  dgreq0  26171  dgrlt  26172  plymul0or  26188  plydiveu  26206  quotcan  26217  aalioulem3  26242  ulmcaulem  26303  sincosq3sgn  26409  sincosq4sgn  26410  sineq0  26433  logrec  26673  xrlimcnp  26878  cxploglim  26888  lgamgulmlem1  26939  mumul  27091  chtub  27123  perfect1  27139  dchrelbas3  27149  lgsdir2lem4  27239  lgsne0  27246  lgsquad2lem2  27296  2sqlem8a  27336  2sqblem  27342  nogt01o  27608  sltlpss  27819  sltadd2im  27893  sltneg  27951  axcontlem2  28892  elntg2  28912  redwlklem  29599  redwlk  29600  crctcshwlkn0lem3  29742  crctcshwlkn0lem5  29744  clwwlkext2edg  29985  wwlksubclwwlk  29987  frgrwopregasn  30245  frgrwopregbsn  30246  blocnilem  30733  ip2eqi  30785  ubthlem2  30800  hial0  31031  hial02  31032  hial2eq  31035  h1datomi  31510  sumspansn  31578  lnopcnbd  31965  riesz4i  31992  bra11  32037  pjss2coi  32093  pjnormssi  32097  pjorthcoi  32098  pjclem4a  32127  pj3lem1  32135  pj3cor1i  32138  hst1h  32156  stm1i  32172  strlem1  32179  golem2  32201  mdbr2  32225  dmdbr5  32237  mdsl2i  32251  atexch  32310  atcvatlem  32314  chirredlem1  32319  cdjreui  32361  cdj1i  32362  cdj3lem1  32363  xraddge02  32680  submarchi  33140  isarchiofld  33295  esumcvg  34076  bnj1468  34836  loop1cycl  35124  erdsze2lem2  35191  btwnexch  36013  btwncolinear2  36058  btwncolinear3  36059  btwncolinear4  36060  btwncolinear5  36061  btwncolinear6  36062  nn0prpw  36311  cldbnd  36314  onsuct0  36429  onint1  36437  bj-ceqsalt0  36872  bj-ceqsalt1  36873  bj-inftyexpiinj  37197  bj-bary1lem1  37299  bj-bary1  37300  relowlssretop  37351  isinf2  37393  ltflcei  37602  tan2h  37606  poimirlem26  37640  poimirlem31  37645  ftc1anclem6  37692  dvasin  37698  dvacos  37699  fdc  37739  caushft  37755  heibor1lem  37803  bfplem2  37817  rrncmslem  37826  rngosn3  37918  mpobi123f  38156  riotasv3d  38953  lsatcv1  39041  lub0N  39182  glb0N  39186  oplecon3b  39193  cmtbr4N  39248  cvrnbtwn2  39268  atnlt  39306  atlatle  39313  cvlsupr2  39336  cvrexchlem  39413  cvratlem  39415  atcvrj0  39422  cvrat4  39437  cvrat42  39438  4noncolr3  39447  ps-1  39471  llnnlt  39517  lplnnlt  39559  lvolnltN  39612  dalempnes  39645  dalemqnet  39646  dalem-cly  39665  dalem44  39710  pmaple  39755  cdlemblem  39787  paddss  39839  2polcon4bN  39912  ltrneq2  40142  cdlemc3  40187  cdleme11h  40260  cdleme16b  40273  cdlemednpq  40293  tendospcanN  41017  dihmeetlem13N  41313  mapdordlem2  41631  mapdn0  41663  rspcsbnea  42119  ccatcan2d  42239  ctbnfien  42806  rmxypairf1o  42900  monotoddzzfi  42931  oddcomabszz  42933  acongtr  42967  onsupnmax  43217  onsupsucismax  43268  frege124d  43750  expgrowth  44324  sbcbi  44529  limsupmnflem  45718  funressnfv  47044  funfocofob  47079  2elfz2melfz  47319  iccpartnel  47439  requad2  47624  grlictr  48007  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem3  48064  uzlidlring  48223  ply1mulgsumlem2  48376  fllog2  48557  dignn0flhalflem1  48604