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  3452  sbceqalOLD  3779  csbiebt  3858  rspcsbela  4366  sneqrg  4767  preq1b  4774  csbexg  5229  elrnrexdm  6947  isoselem  7192  riotass2  7243  ordzsl  7667  oaword2  8346  oaordex  8351  omword1  8366  om00  8368  omeulem2  8376  oen0  8379  oeeui  8395  nnaordex  8431  php3  8899  onomeneq  8943  frfi  8989  infglb  9179  suc11reg  9307  cardne  9654  cardsdomel  9663  carduni  9670  acndom  9738  alephinit  9782  cfflb  9946  cfslb2n  9955  fin23lem28  10027  isf34lem6  10067  fin1a2lem9  10095  axcc3  10125  winalim2  10383  inar1  10462  rankcf  10464  addclprlem2  10704  mulclprlem  10706  ltexprlem7  10729  prlem936  10734  reclem4pr  10737  sqgt0sr  10793  ltord2  11434  leord2  11435  eqord2  11436  mulgt1  11764  mulge0b  11775  lt2halves  12138  addltmul  12139  ltsubnn0  12214  nzadd  12298  zextlt  12324  recnz  12325  zeo  12336  peano5uzi  12339  uzm1  12545  irradd  12642  irrmul  12643  xltneg  12880  xleadd1  12918  xmulasslem  12948  xlemul1a  12951  xlemul1  12953  fznuz  13267  uznfz  13268  axdc4uzlem  13631  facndiv  13930  hashvnfin  14003  hashgt12el  14065  hashgt12el2  14066  hashf1  14099  ccatalpha  14226  swrdccatin2  14370  swrdccatin2d  14385  rennim  14878  cau3lem  14994  caubnd2  14997  o1lo1  15174  climrlim2  15184  climshft  15213  subcn2  15232  mulcn2  15233  rlimo1  15254  o1dif  15267  isercoll  15307  caucvgrlem  15312  serf0  15320  cvgrat  15523  efieq1re  15836  moddvds  15902  dvdsssfz1  15955  smuval2  16117  nn0seqcvgd  16203  algcvgblem  16210  eucalglt  16218  lcmgcdlem  16239  rpmul  16292  divgcdcoprm0  16298  isprm6  16347  rpexp  16355  eulerthlem2  16411  prmdiv  16414  pcprendvds2  16470  pcz  16510  pcprmpw  16512  pcadd2  16519  pcfac  16528  expnprm  16531  ramlb  16648  firest  17060  joineu  18015  meeteu  18029  latjlej1  18086  latjlej2  18087  latmlem1  18102  latmlem2  18103  lubun  18148  acsmapd  18187  imasgrp2  18605  issubg4  18689  psgnunilem4  19020  oddvdsnn0  19067  odmulgeq  19079  subgpgp  19117  odcau  19124  lsmlub  19185  frgpnabllem1  19389  pgpfac1lem2  19593  pgpfac1lem3a  19594  pgpfac1lem3  19595  irredrmul  19864  islmhm2  20215  lsmelval2  20262  lspsnat  20322  znidomb  20681  ip2eq  20770  lsmcss  20809  cnpnei  22323  cncls2  22332  cncls  22333  cnntr  22334  cnt0  22405  isnrm2  22417  comppfsc  22591  kqcldsat  22792  isr0  22796  hmeoopn  22825  hmeocld  22826  trufil  22969  opnsubg  23167  ghmcnp  23174  tgphaus  23176  qustgpopn  23179  tsmsgsum  23198  isngp4  23674  xrhmeo  24015  bndth  24027  cfilres  24365  caubl  24377  ivthlem2  24521  ovolicc2  24591  ismbf3d  24723  itg1ge0a  24781  mbfi1flim  24793  itg2gt0  24830  dvge0  25075  dvcnvrelem1  25086  dvcvx  25089  mdegmullem  25148  ig1peu  25241  plyco  25307  coemulc  25321  dgreq0  25331  dgrlt  25332  plymul0or  25346  plydiveu  25363  quotcan  25374  aalioulem3  25399  ulmcaulem  25458  sincosq3sgn  25562  sincosq4sgn  25563  sineq0  25585  logrec  25818  xrlimcnp  26023  cxploglim  26032  lgamgulmlem1  26083  mumul  26235  chtub  26265  perfect1  26281  dchrelbas3  26291  lgsdir2lem4  26381  lgsne0  26388  lgsquad2lem2  26438  2sqlem8a  26478  2sqblem  26484  axcontlem2  27236  elntg2  27256  redwlklem  27941  redwlk  27942  crctcshwlkn0lem3  28078  crctcshwlkn0lem5  28080  clwwlkext2edg  28321  wwlksubclwwlk  28323  frgrwopregasn  28581  frgrwopregbsn  28582  blocnilem  29067  ip2eqi  29119  ubthlem2  29134  hial0  29365  hial02  29366  hial2eq  29369  h1datomi  29844  sumspansn  29912  lnopcnbd  30299  riesz4i  30326  bra11  30371  pjss2coi  30427  pjnormssi  30431  pjorthcoi  30432  pjclem4a  30461  pj3lem1  30469  pj3cor1i  30472  hst1h  30490  stm1i  30506  strlem1  30513  golem2  30535  mdbr2  30559  dmdbr5  30571  mdsl2i  30585  atexch  30644  atcvatlem  30648  chirredlem1  30653  cdjreui  30695  cdj1i  30696  cdj3lem1  30697  xraddge02  30981  submarchi  31342  isarchiofld  31418  esumcvg  31954  bnj1468  32726  loop1cycl  32999  erdsze2lem2  33066  funeldmb  33643  nogt01o  33826  sltlpss  34014  btwnexch  34254  btwncolinear2  34299  btwncolinear3  34300  btwncolinear4  34301  btwncolinear5  34302  btwncolinear6  34303  nn0prpw  34439  cldbnd  34442  onsuct0  34557  onint1  34565  bj-ceqsalt0  34996  bj-ceqsalt1  34997  bj-inftyexpiinj  35307  bj-bary1lem1  35409  bj-bary1  35410  relowlssretop  35461  isinf2  35503  ltflcei  35692  tan2h  35696  poimirlem26  35730  poimirlem31  35735  ftc1anclem6  35782  dvasin  35788  dvacos  35789  fdc  35830  caushft  35846  heibor1lem  35894  bfplem2  35908  rrncmslem  35917  rngosn3  36009  mpobi123f  36247  riotasv3d  36901  lsatcv1  36989  lub0N  37130  glb0N  37134  oplecon3b  37141  cmtbr4N  37196  cvrnbtwn2  37216  atnlt  37254  atlatle  37261  cvlsupr2  37284  cvrexchlem  37360  cvratlem  37362  atcvrj0  37369  cvrat4  37384  cvrat42  37385  4noncolr3  37394  ps-1  37418  llnnlt  37464  lplnnlt  37506  lvolnltN  37559  dalempnes  37592  dalemqnet  37593  dalem-cly  37612  dalem44  37657  pmaple  37702  cdlemblem  37734  paddss  37786  2polcon4bN  37859  ltrneq2  38089  cdlemc3  38134  cdleme11h  38207  cdleme16b  38220  cdlemednpq  38240  tendospcanN  38964  dihmeetlem13N  39260  mapdordlem2  39578  mapdn0  39610  isdomn4  40100  ccatcan2d  40145  ctbnfien  40556  rmxypairf1o  40649  monotoddzzfi  40680  oddcomabszz  40682  acongtr  40716  frege124d  41258  expgrowth  41842  sbcbi  42048  limsupmnflem  43151  funressnfv  44424  funfocofob  44457  2elfz2melfz  44698  iccpartnel  44778  requad2  44963  uzlidlring  45375  ply1mulgsumlem2  45616  fllog2  45802  dignn0flhalflem1  45849