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  sbceqalOLD  3871  csbiebt  3951  rspcsbela  4461  sneqrg  4864  preq1b  4871  csbexg  5328  elrnrexdm  7123  isoselem  7377  funeldmb  7395  riotass2  7435  ordzsl  7882  oaword2  8609  oaordex  8614  omword1  8629  om00  8631  omeulem2  8639  oen0  8642  oeeui  8658  nnaordex  8694  php3  9275  php3OLD  9287  onomeneqOLD  9292  frfi  9349  infglb  9559  suc11reg  9688  cardne  10034  cardsdomel  10043  carduni  10050  acndom  10120  alephinit  10164  cfflb  10328  cfslb2n  10337  fin23lem28  10409  isf34lem6  10449  fin1a2lem9  10477  axcc3  10507  winalim2  10765  inar1  10844  rankcf  10846  addclprlem2  11086  mulclprlem  11088  ltexprlem7  11111  prlem936  11116  reclem4pr  11119  sqgt0sr  11175  ltord2  11819  leord2  11820  eqord2  11821  mulgt1OLD  12153  mulge0b  12165  lt2halves  12528  addltmul  12529  ltsubnn0  12604  nzadd  12691  zextlt  12717  recnz  12718  zeo  12729  peano5uzi  12732  uzm1  12941  irradd  13038  irrmul  13039  xltneg  13279  xleadd1  13317  xmulasslem  13347  xlemul1a  13350  xlemul1  13352  fznuz  13666  uznfz  13667  axdc4uzlem  14034  facndiv  14337  hashvnfin  14409  hashgt12el  14471  hashgt12el2  14472  hashf1  14506  ccatalpha  14641  swrdccatin2  14777  swrdccatin2d  14792  rennim  15288  cau3lem  15403  caubnd2  15406  o1lo1  15583  climrlim2  15593  climshft  15622  subcn2  15641  mulcn2  15642  rlimo1  15663  o1dif  15676  isercoll  15716  caucvgrlem  15721  serf0  15729  cvgrat  15931  efieq1re  16247  moddvds  16313  dvdsssfz1  16366  smuval2  16528  nn0seqcvgd  16617  algcvgblem  16624  eucalglt  16632  lcmgcdlem  16653  rpmul  16706  divgcdcoprm0  16712  isprm6  16761  rpexp  16769  eulerthlem2  16829  prmdiv  16832  pcprendvds2  16888  pcz  16928  pcprmpw  16930  pcadd2  16937  pcfac  16946  expnprm  16949  ramlb  17066  firest  17492  joineu  18452  meeteu  18466  latjlej1  18523  latjlej2  18524  latmlem1  18539  latmlem2  18540  lubun  18585  acsmapd  18624  imasgrp2  19095  issubg4  19185  psgnunilem4  19539  oddvdsnn0  19586  odmulgeq  19599  subgpgp  19639  odcau  19646  lsmlub  19706  frgpnabllem1  19915  pgpfac1lem2  20119  pgpfac1lem3a  20120  pgpfac1lem3  20121  irredrmul  20453  isdomn4  20738  islmhm2  21060  lsmelval2  21107  lspsnat  21170  znidomb  21603  ip2eq  21694  lsmcss  21733  cnpnei  23293  cncls2  23302  cncls  23303  cnntr  23304  cnt0  23375  isnrm2  23387  comppfsc  23561  kqcldsat  23762  isr0  23766  hmeoopn  23795  hmeocld  23796  trufil  23939  opnsubg  24137  ghmcnp  24144  tgphaus  24146  qustgpopn  24149  tsmsgsum  24168  isngp4  24646  xrhmeo  24996  bndth  25009  cfilres  25349  caubl  25361  ivthlem2  25506  ovolicc2  25576  ismbf3d  25708  itg1ge0a  25766  mbfi1flim  25778  itg2gt0  25815  dvge0  26065  dvcnvrelem1  26076  dvcvx  26079  mdegmullem  26137  ig1peu  26234  plyco  26300  coemulc  26314  dgreq0  26325  dgrlt  26326  plymul0or  26340  plydiveu  26358  quotcan  26369  aalioulem3  26394  ulmcaulem  26455  sincosq3sgn  26560  sincosq4sgn  26561  sineq0  26584  logrec  26824  xrlimcnp  27029  cxploglim  27039  lgamgulmlem1  27090  mumul  27242  chtub  27274  perfect1  27290  dchrelbas3  27300  lgsdir2lem4  27390  lgsne0  27397  lgsquad2lem2  27447  2sqlem8a  27487  2sqblem  27493  nogt01o  27759  sltlpss  27963  sltadd2im  28037  sltneg  28095  axcontlem2  28998  elntg2  29018  redwlklem  29707  redwlk  29708  crctcshwlkn0lem3  29845  crctcshwlkn0lem5  29847  clwwlkext2edg  30088  wwlksubclwwlk  30090  frgrwopregasn  30348  frgrwopregbsn  30349  blocnilem  30836  ip2eqi  30888  ubthlem2  30903  hial0  31134  hial02  31135  hial2eq  31138  h1datomi  31613  sumspansn  31681  lnopcnbd  32068  riesz4i  32095  bra11  32140  pjss2coi  32196  pjnormssi  32200  pjorthcoi  32201  pjclem4a  32230  pj3lem1  32238  pj3cor1i  32241  hst1h  32259  stm1i  32275  strlem1  32282  golem2  32304  mdbr2  32328  dmdbr5  32340  mdsl2i  32354  atexch  32413  atcvatlem  32417  chirredlem1  32422  cdjreui  32464  cdj1i  32465  cdj3lem1  32466  xraddge02  32763  submarchi  33166  isarchiofld  33312  esumcvg  34050  bnj1468  34822  loop1cycl  35105  erdsze2lem2  35172  btwnexch  35989  btwncolinear2  36034  btwncolinear3  36035  btwncolinear4  36036  btwncolinear5  36037  btwncolinear6  36038  nn0prpw  36289  cldbnd  36292  onsuct0  36407  onint1  36415  bj-ceqsalt0  36850  bj-ceqsalt1  36851  bj-inftyexpiinj  37175  bj-bary1lem1  37277  bj-bary1  37278  relowlssretop  37329  isinf2  37371  ltflcei  37568  tan2h  37572  poimirlem26  37606  poimirlem31  37611  ftc1anclem6  37658  dvasin  37664  dvacos  37665  fdc  37705  caushft  37721  heibor1lem  37769  bfplem2  37783  rrncmslem  37792  rngosn3  37884  mpobi123f  38122  riotasv3d  38916  lsatcv1  39004  lub0N  39145  glb0N  39149  oplecon3b  39156  cmtbr4N  39211  cvrnbtwn2  39231  atnlt  39269  atlatle  39276  cvlsupr2  39299  cvrexchlem  39376  cvratlem  39378  atcvrj0  39385  cvrat4  39400  cvrat42  39401  4noncolr3  39410  ps-1  39434  llnnlt  39480  lplnnlt  39522  lvolnltN  39575  dalempnes  39608  dalemqnet  39609  dalem-cly  39628  dalem44  39673  pmaple  39718  cdlemblem  39750  paddss  39802  2polcon4bN  39875  ltrneq2  40105  cdlemc3  40150  cdleme11h  40223  cdleme16b  40236  cdlemednpq  40256  tendospcanN  40980  dihmeetlem13N  41276  mapdordlem2  41594  mapdn0  41626  rspcsbnea  42088  ccatcan2d  42246  ctbnfien  42774  rmxypairf1o  42868  monotoddzzfi  42899  oddcomabszz  42901  acongtr  42935  onsupnmax  43189  onsupsucismax  43241  frege124d  43723  expgrowth  44304  sbcbi  44510  limsupmnflem  45641  funressnfv  46958  funfocofob  46993  2elfz2melfz  47233  iccpartnel  47312  requad2  47497  grlictr  47832  uzlidlring  47958  ply1mulgsumlem2  48116  fllog2  48302  dignn0flhalflem1  48349