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  293  sbceqalOLD  3844  csbiebt  3923  rspcsbela  4435  sneqrg  4840  preq1b  4847  csbexg  5310  elrnrexdm  7088  isoselem  7335  funeldmb  7353  riotass2  7393  ordzsl  7831  oaword2  8550  oaordex  8555  omword1  8570  om00  8572  omeulem2  8580  oen0  8583  oeeui  8599  nnaordex  8635  php3  9209  php3OLD  9221  onomeneqOLD  9226  frfi  9285  infglb  9482  suc11reg  9611  cardne  9957  cardsdomel  9966  carduni  9973  acndom  10043  alephinit  10087  cfflb  10251  cfslb2n  10260  fin23lem28  10332  isf34lem6  10372  fin1a2lem9  10400  axcc3  10430  winalim2  10688  inar1  10767  rankcf  10769  addclprlem2  11009  mulclprlem  11011  ltexprlem7  11034  prlem936  11039  reclem4pr  11042  sqgt0sr  11098  ltord2  11740  leord2  11741  eqord2  11742  mulgt1  12070  mulge0b  12081  lt2halves  12444  addltmul  12445  ltsubnn0  12520  nzadd  12607  zextlt  12633  recnz  12634  zeo  12645  peano5uzi  12648  uzm1  12857  irradd  12954  irrmul  12955  xltneg  13193  xleadd1  13231  xmulasslem  13261  xlemul1a  13264  xlemul1  13266  fznuz  13580  uznfz  13581  axdc4uzlem  13945  facndiv  14245  hashvnfin  14317  hashgt12el  14379  hashgt12el2  14380  hashf1  14415  ccatalpha  14540  swrdccatin2  14676  swrdccatin2d  14691  rennim  15183  cau3lem  15298  caubnd2  15301  o1lo1  15478  climrlim2  15488  climshft  15517  subcn2  15536  mulcn2  15537  rlimo1  15558  o1dif  15571  isercoll  15611  caucvgrlem  15616  serf0  15624  cvgrat  15826  efieq1re  16139  moddvds  16205  dvdsssfz1  16258  smuval2  16420  nn0seqcvgd  16504  algcvgblem  16511  eucalglt  16519  lcmgcdlem  16540  rpmul  16593  divgcdcoprm0  16599  isprm6  16648  rpexp  16656  eulerthlem2  16712  prmdiv  16715  pcprendvds2  16771  pcz  16811  pcprmpw  16813  pcadd2  16820  pcfac  16829  expnprm  16832  ramlb  16949  firest  17375  joineu  18332  meeteu  18346  latjlej1  18403  latjlej2  18404  latmlem1  18419  latmlem2  18420  lubun  18465  acsmapd  18504  imasgrp2  18935  issubg4  19020  psgnunilem4  19360  oddvdsnn0  19407  odmulgeq  19420  subgpgp  19460  odcau  19467  lsmlub  19527  frgpnabllem1  19736  pgpfac1lem2  19940  pgpfac1lem3a  19941  pgpfac1lem3  19942  irredrmul  20234  islmhm2  20642  lsmelval2  20689  lspsnat  20751  isdomn4  20911  znidomb  21109  ip2eq  21198  lsmcss  21237  cnpnei  22760  cncls2  22769  cncls  22770  cnntr  22771  cnt0  22842  isnrm2  22854  comppfsc  23028  kqcldsat  23229  isr0  23233  hmeoopn  23262  hmeocld  23263  trufil  23406  opnsubg  23604  ghmcnp  23611  tgphaus  23613  qustgpopn  23616  tsmsgsum  23635  isngp4  24113  xrhmeo  24454  bndth  24466  cfilres  24805  caubl  24817  ivthlem2  24961  ovolicc2  25031  ismbf3d  25163  itg1ge0a  25221  mbfi1flim  25233  itg2gt0  25270  dvge0  25515  dvcnvrelem1  25526  dvcvx  25529  mdegmullem  25588  ig1peu  25681  plyco  25747  coemulc  25761  dgreq0  25771  dgrlt  25772  plymul0or  25786  plydiveu  25803  quotcan  25814  aalioulem3  25839  ulmcaulem  25898  sincosq3sgn  26002  sincosq4sgn  26003  sineq0  26025  logrec  26258  xrlimcnp  26463  cxploglim  26472  lgamgulmlem1  26523  mumul  26675  chtub  26705  perfect1  26721  dchrelbas3  26731  lgsdir2lem4  26821  lgsne0  26828  lgsquad2lem2  26878  2sqlem8a  26918  2sqblem  26924  nogt01o  27189  sltlpss  27391  sltadd2im  27459  sltneg  27509  axcontlem2  28213  elntg2  28233  redwlklem  28918  redwlk  28919  crctcshwlkn0lem3  29056  crctcshwlkn0lem5  29058  clwwlkext2edg  29299  wwlksubclwwlk  29301  frgrwopregasn  29559  frgrwopregbsn  29560  blocnilem  30045  ip2eqi  30097  ubthlem2  30112  hial0  30343  hial02  30344  hial2eq  30347  h1datomi  30822  sumspansn  30890  lnopcnbd  31277  riesz4i  31304  bra11  31349  pjss2coi  31405  pjnormssi  31409  pjorthcoi  31410  pjclem4a  31439  pj3lem1  31447  pj3cor1i  31450  hst1h  31468  stm1i  31484  strlem1  31491  golem2  31513  mdbr2  31537  dmdbr5  31549  mdsl2i  31563  atexch  31622  atcvatlem  31626  chirredlem1  31631  cdjreui  31673  cdj1i  31674  cdj3lem1  31675  xraddge02  31957  submarchi  32320  isarchiofld  32424  esumcvg  33073  bnj1468  33846  loop1cycl  34117  erdsze2lem2  34184  btwnexch  34986  btwncolinear2  35031  btwncolinear3  35032  btwncolinear4  35033  btwncolinear5  35034  btwncolinear6  35035  nn0prpw  35197  cldbnd  35200  onsuct0  35315  onint1  35323  bj-ceqsalt0  35753  bj-ceqsalt1  35754  bj-inftyexpiinj  36079  bj-bary1lem1  36181  bj-bary1  36182  relowlssretop  36233  isinf2  36275  ltflcei  36465  tan2h  36469  poimirlem26  36503  poimirlem31  36508  ftc1anclem6  36555  dvasin  36561  dvacos  36562  fdc  36602  caushft  36618  heibor1lem  36666  bfplem2  36680  rrncmslem  36689  rngosn3  36781  mpobi123f  37019  riotasv3d  37819  lsatcv1  37907  lub0N  38048  glb0N  38052  oplecon3b  38059  cmtbr4N  38114  cvrnbtwn2  38134  atnlt  38172  atlatle  38179  cvlsupr2  38202  cvrexchlem  38279  cvratlem  38281  atcvrj0  38288  cvrat4  38303  cvrat42  38304  4noncolr3  38313  ps-1  38337  llnnlt  38383  lplnnlt  38425  lvolnltN  38478  dalempnes  38511  dalemqnet  38512  dalem-cly  38531  dalem44  38576  pmaple  38621  cdlemblem  38653  paddss  38705  2polcon4bN  38778  ltrneq2  39008  cdlemc3  39053  cdleme11h  39126  cdleme16b  39139  cdlemednpq  39159  tendospcanN  39883  dihmeetlem13N  40179  mapdordlem2  40497  mapdn0  40529  ccatcan2d  41067  ctbnfien  41542  rmxypairf1o  41636  monotoddzzfi  41667  oddcomabszz  41669  acongtr  41703  onsupnmax  41963  onsupsucismax  42015  frege124d  42498  expgrowth  43080  sbcbi  43286  limsupmnflem  44423  funressnfv  45740  funfocofob  45773  2elfz2melfz  46013  iccpartnel  46093  requad2  46278  uzlidlring  46781  ply1mulgsumlem2  47022  fllog2  47208  dignn0flhalflem1  47255