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  3879  rspcsbela  4388  sneqrg  4791  preq1b  4798  csbexg  5248  elrnrexdm  7022  isoselem  7275  funeldmb  7293  riotass2  7333  ordzsl  7775  resf1extb  7864  oaword2  8468  oaordex  8473  omword1  8488  om00  8490  omeulem2  8498  oen0  8501  oeeui  8517  nnaordex  8553  php3  9118  frfi  9169  infglb  9375  suc11reg  9509  cardne  9855  cardsdomel  9864  carduni  9871  acndom  9939  alephinit  9983  cfflb  10147  cfslb2n  10156  fin23lem28  10228  isf34lem6  10268  fin1a2lem9  10296  axcc3  10326  winalim2  10584  inar1  10663  rankcf  10665  addclprlem2  10905  mulclprlem  10907  ltexprlem7  10930  prlem936  10935  reclem4pr  10938  sqgt0sr  10994  ltord2  11643  leord2  11644  eqord2  11645  mulgt1OLD  11977  mulge0b  11989  lt2halves  12353  addltmul  12354  ltsubnn0  12429  nzadd  12517  zextlt  12544  recnz  12545  zeo  12556  peano5uzi  12559  uzm1  12767  irradd  12868  irrmul  12869  xltneg  13113  xleadd1  13151  xmulasslem  13181  xlemul1a  13184  xlemul1  13186  fznuz  13506  uznfz  13507  axdc4uzlem  13887  facndiv  14192  hashvnfin  14264  hashgt12el  14326  hashgt12el2  14327  hashf1  14361  ccatalpha  14498  swrdccatin2  14633  swrdccatin2d  14648  rennim  15143  cau3lem  15259  caubnd2  15262  o1lo1  15441  climrlim2  15451  climshft  15480  subcn2  15499  mulcn2  15500  rlimo1  15521  o1dif  15534  isercoll  15572  caucvgrlem  15577  serf0  15585  cvgrat  15787  efieq1re  16105  moddvds  16171  dvdsssfz1  16226  smuval2  16390  nn0seqcvgd  16478  algcvgblem  16485  eucalglt  16493  lcmgcdlem  16514  rpmul  16567  divgcdcoprm0  16573  isprm6  16622  rpexp  16630  eulerthlem2  16690  prmdiv  16693  pcprendvds2  16750  pcz  16790  pcprmpw  16792  pcadd2  16799  pcfac  16808  expnprm  16811  ramlb  16928  firest  17333  joineu  18283  meeteu  18297  latjlej1  18356  latjlej2  18357  latmlem1  18372  latmlem2  18373  lubun  18418  acsmapd  18457  imasgrp2  18965  issubg4  19055  psgnunilem4  19407  oddvdsnn0  19454  odmulgeq  19467  subgpgp  19507  odcau  19514  lsmlub  19574  frgpnabllem1  19783  pgpfac1lem2  19987  pgpfac1lem3a  19988  pgpfac1lem3  19989  irredrmul  20343  isdomn4  20629  islmhm2  20970  lsmelval2  21017  lspsnat  21080  znidomb  21496  ip2eq  21588  lsmcss  21627  cnpnei  23177  cncls2  23186  cncls  23187  cnntr  23188  cnt0  23259  isnrm2  23271  comppfsc  23445  kqcldsat  23646  isr0  23650  hmeoopn  23679  hmeocld  23680  trufil  23823  opnsubg  24021  ghmcnp  24028  tgphaus  24030  qustgpopn  24033  tsmsgsum  24052  isngp4  24525  xrhmeo  24869  bndth  24882  cfilres  25221  caubl  25233  ivthlem2  25378  ovolicc2  25448  ismbf3d  25580  itg1ge0a  25637  mbfi1flim  25649  itg2gt0  25686  dvge0  25936  dvcnvrelem1  25947  dvcvx  25950  mdegmullem  26008  ig1peu  26105  plyco  26171  coemulc  26185  dgreq0  26196  dgrlt  26197  plymul0or  26213  plydiveu  26231  quotcan  26242  aalioulem3  26267  ulmcaulem  26328  sincosq3sgn  26434  sincosq4sgn  26435  sineq0  26458  logrec  26698  xrlimcnp  26903  cxploglim  26913  lgamgulmlem1  26964  mumul  27116  chtub  27148  perfect1  27164  dchrelbas3  27174  lgsdir2lem4  27264  lgsne0  27271  lgsquad2lem2  27321  2sqlem8a  27361  2sqblem  27367  nogt01o  27633  sltlpss  27851  sltadd2im  27927  sltneg  27985  axcontlem2  28941  elntg2  28961  redwlklem  29646  redwlk  29647  crctcshwlkn0lem3  29788  crctcshwlkn0lem5  29790  clwwlkext2edg  30031  wwlksubclwwlk  30033  frgrwopregasn  30291  frgrwopregbsn  30292  blocnilem  30779  ip2eqi  30831  ubthlem2  30846  hial0  31077  hial02  31078  hial2eq  31081  h1datomi  31556  sumspansn  31624  lnopcnbd  32011  riesz4i  32038  bra11  32083  pjss2coi  32139  pjnormssi  32143  pjorthcoi  32144  pjclem4a  32173  pj3lem1  32181  pj3cor1i  32184  hst1h  32202  stm1i  32218  strlem1  32225  golem2  32247  mdbr2  32271  dmdbr5  32283  mdsl2i  32297  atexch  32356  atcvatlem  32360  chirredlem1  32365  cdjreui  32407  cdj1i  32408  cdj3lem1  32409  xraddge02  32735  submarchi  33150  isarchiofld  33163  esumcvg  34094  bnj1468  34853  loop1cycl  35169  erdsze2lem2  35236  btwnexch  36058  btwncolinear2  36103  btwncolinear3  36104  btwncolinear4  36105  btwncolinear5  36106  btwncolinear6  36107  nn0prpw  36356  cldbnd  36359  onsuct0  36474  onint1  36482  bj-ceqsalt0  36917  bj-ceqsalt1  36918  bj-inftyexpiinj  37242  bj-bary1lem1  37344  bj-bary1  37345  relowlssretop  37396  isinf2  37438  ltflcei  37647  tan2h  37651  poimirlem26  37685  poimirlem31  37690  ftc1anclem6  37737  dvasin  37743  dvacos  37744  fdc  37784  caushft  37800  heibor1lem  37848  bfplem2  37862  rrncmslem  37871  rngosn3  37963  mpobi123f  38201  riotasv3d  38998  lsatcv1  39086  lub0N  39227  glb0N  39231  oplecon3b  39238  cmtbr4N  39293  cvrnbtwn2  39313  atnlt  39351  atlatle  39358  cvlsupr2  39381  cvrexchlem  39457  cvratlem  39459  atcvrj0  39466  cvrat4  39481  cvrat42  39482  4noncolr3  39491  ps-1  39515  llnnlt  39561  lplnnlt  39603  lvolnltN  39656  dalempnes  39689  dalemqnet  39690  dalem-cly  39709  dalem44  39754  pmaple  39799  cdlemblem  39831  paddss  39883  2polcon4bN  39956  ltrneq2  40186  cdlemc3  40231  cdleme11h  40304  cdleme16b  40317  cdlemednpq  40337  tendospcanN  41061  dihmeetlem13N  41357  mapdordlem2  41675  mapdn0  41707  rspcsbnea  42163  ccatcan2d  42283  ctbnfien  42850  rmxypairf1o  42943  monotoddzzfi  42974  oddcomabszz  42976  acongtr  43010  onsupnmax  43260  onsupsucismax  43311  frege124d  43793  expgrowth  44367  sbcbi  44571  limsupmnflem  45757  funressnfv  47073  funfocofob  47108  2elfz2melfz  47348  iccpartnel  47468  requad2  47653  grlictr  48045  gpg5nbgrvtx13starlem1  48101  gpg5nbgrvtx13starlem3  48103  uzlidlring  48265  ply1mulgsumlem2  48418  fllog2  48599  dignn0flhalflem1  48646