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  sbceqalOLD  3840  csbiebt  3919  rspcsbela  4437  sneqrg  4842  preq1b  4849  csbexg  5311  elrnrexdm  7098  isoselem  7348  funeldmb  7366  riotass2  7406  ordzsl  7850  oaword2  8574  oaordex  8579  omword1  8594  om00  8596  omeulem2  8604  oen0  8607  oeeui  8623  nnaordex  8659  php3  9237  php3OLD  9249  onomeneqOLD  9254  frfi  9313  infglb  9515  suc11reg  9644  cardne  9990  cardsdomel  9999  carduni  10006  acndom  10076  alephinit  10120  cfflb  10284  cfslb2n  10293  fin23lem28  10365  isf34lem6  10405  fin1a2lem9  10433  axcc3  10463  winalim2  10721  inar1  10800  rankcf  10802  addclprlem2  11042  mulclprlem  11044  ltexprlem7  11067  prlem936  11072  reclem4pr  11075  sqgt0sr  11131  ltord2  11775  leord2  11776  eqord2  11777  mulgt1  12106  mulge0b  12117  lt2halves  12480  addltmul  12481  ltsubnn0  12556  nzadd  12643  zextlt  12669  recnz  12670  zeo  12681  peano5uzi  12684  uzm1  12893  irradd  12990  irrmul  12991  xltneg  13231  xleadd1  13269  xmulasslem  13299  xlemul1a  13302  xlemul1  13304  fznuz  13618  uznfz  13619  axdc4uzlem  13984  facndiv  14283  hashvnfin  14355  hashgt12el  14417  hashgt12el2  14418  hashf1  14454  ccatalpha  14579  swrdccatin2  14715  swrdccatin2d  14730  rennim  15222  cau3lem  15337  caubnd2  15340  o1lo1  15517  climrlim2  15527  climshft  15556  subcn2  15575  mulcn2  15576  rlimo1  15597  o1dif  15610  isercoll  15650  caucvgrlem  15655  serf0  15663  cvgrat  15865  efieq1re  16179  moddvds  16245  dvdsssfz1  16298  smuval2  16460  nn0seqcvgd  16544  algcvgblem  16551  eucalglt  16559  lcmgcdlem  16580  rpmul  16633  divgcdcoprm0  16639  isprm6  16688  rpexp  16697  eulerthlem2  16754  prmdiv  16757  pcprendvds2  16813  pcz  16853  pcprmpw  16855  pcadd2  16862  pcfac  16871  expnprm  16874  ramlb  16991  firest  17417  joineu  18377  meeteu  18391  latjlej1  18448  latjlej2  18449  latmlem1  18464  latmlem2  18465  lubun  18510  acsmapd  18549  imasgrp2  19019  issubg4  19108  psgnunilem4  19464  oddvdsnn0  19511  odmulgeq  19524  subgpgp  19564  odcau  19571  lsmlub  19631  frgpnabllem1  19840  pgpfac1lem2  20044  pgpfac1lem3a  20045  pgpfac1lem3  20046  irredrmul  20378  islmhm2  20935  lsmelval2  20982  lspsnat  21045  isdomn4  21267  znidomb  21512  ip2eq  21602  lsmcss  21641  cnpnei  23212  cncls2  23221  cncls  23222  cnntr  23223  cnt0  23294  isnrm2  23306  comppfsc  23480  kqcldsat  23681  isr0  23685  hmeoopn  23714  hmeocld  23715  trufil  23858  opnsubg  24056  ghmcnp  24063  tgphaus  24065  qustgpopn  24068  tsmsgsum  24087  isngp4  24565  xrhmeo  24915  bndth  24928  cfilres  25268  caubl  25280  ivthlem2  25425  ovolicc2  25495  ismbf3d  25627  itg1ge0a  25685  mbfi1flim  25697  itg2gt0  25734  dvge0  25983  dvcnvrelem1  25994  dvcvx  25997  mdegmullem  26058  ig1peu  26154  plyco  26220  coemulc  26234  dgreq0  26245  dgrlt  26246  plymul0or  26260  plydiveu  26278  quotcan  26289  aalioulem3  26314  ulmcaulem  26375  sincosq3sgn  26480  sincosq4sgn  26481  sineq0  26503  logrec  26740  xrlimcnp  26945  cxploglim  26955  lgamgulmlem1  27006  mumul  27158  chtub  27190  perfect1  27206  dchrelbas3  27216  lgsdir2lem4  27306  lgsne0  27313  lgsquad2lem2  27363  2sqlem8a  27403  2sqblem  27409  nogt01o  27675  sltlpss  27879  sltadd2im  27949  sltneg  28003  axcontlem2  28848  elntg2  28868  redwlklem  29557  redwlk  29558  crctcshwlkn0lem3  29695  crctcshwlkn0lem5  29697  clwwlkext2edg  29938  wwlksubclwwlk  29940  frgrwopregasn  30198  frgrwopregbsn  30199  blocnilem  30686  ip2eqi  30738  ubthlem2  30753  hial0  30984  hial02  30985  hial2eq  30988  h1datomi  31463  sumspansn  31531  lnopcnbd  31918  riesz4i  31945  bra11  31990  pjss2coi  32046  pjnormssi  32050  pjorthcoi  32051  pjclem4a  32080  pj3lem1  32088  pj3cor1i  32091  hst1h  32109  stm1i  32125  strlem1  32132  golem2  32154  mdbr2  32178  dmdbr5  32190  mdsl2i  32204  atexch  32263  atcvatlem  32267  chirredlem1  32272  cdjreui  32314  cdj1i  32315  cdj3lem1  32316  xraddge02  32608  submarchi  32986  isarchiofld  33131  esumcvg  33836  bnj1468  34608  loop1cycl  34878  erdsze2lem2  34945  btwnexch  35752  btwncolinear2  35797  btwncolinear3  35798  btwncolinear4  35799  btwncolinear5  35800  btwncolinear6  35801  nn0prpw  35938  cldbnd  35941  onsuct0  36056  onint1  36064  bj-ceqsalt0  36493  bj-ceqsalt1  36494  bj-inftyexpiinj  36819  bj-bary1lem1  36921  bj-bary1  36922  relowlssretop  36973  isinf2  37015  ltflcei  37212  tan2h  37216  poimirlem26  37250  poimirlem31  37255  ftc1anclem6  37302  dvasin  37308  dvacos  37309  fdc  37349  caushft  37365  heibor1lem  37413  bfplem2  37427  rrncmslem  37436  rngosn3  37528  mpobi123f  37766  riotasv3d  38562  lsatcv1  38650  lub0N  38791  glb0N  38795  oplecon3b  38802  cmtbr4N  38857  cvrnbtwn2  38877  atnlt  38915  atlatle  38922  cvlsupr2  38945  cvrexchlem  39022  cvratlem  39024  atcvrj0  39031  cvrat4  39046  cvrat42  39047  4noncolr3  39056  ps-1  39080  llnnlt  39126  lplnnlt  39168  lvolnltN  39221  dalempnes  39254  dalemqnet  39255  dalem-cly  39274  dalem44  39319  pmaple  39364  cdlemblem  39396  paddss  39448  2polcon4bN  39521  ltrneq2  39751  cdlemc3  39796  cdleme11h  39869  cdleme16b  39882  cdlemednpq  39902  tendospcanN  40626  dihmeetlem13N  40922  mapdordlem2  41240  mapdn0  41272  rspcsbnea  41734  ccatcan2d  41873  ctbnfien  42380  rmxypairf1o  42474  monotoddzzfi  42505  oddcomabszz  42507  acongtr  42541  onsupnmax  42798  onsupsucismax  42850  frege124d  43333  expgrowth  43914  sbcbi  44120  limsupmnflem  45246  funressnfv  46563  funfocofob  46596  2elfz2melfz  46836  iccpartnel  46915  requad2  47100  uzlidlring  47483  ply1mulgsumlem2  47641  fllog2  47827  dignn0flhalflem1  47874