Theorem sylibd 242

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 232	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 48	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3imtr3d  296  csbiebt  3884  rspcsbela  4395  sneqrg  4799  preq1b  4806  csbexg  5264  elrnrexdm  7074  isoselem  7329  funeldmb  7347  riotass2  7387  ordzsl  7829  resf1extb  7919  oaword2  8526  oaordex  8531  omword1  8546  om00  8548  omeulem2  8556  oen0  8560  oeeui  8576  nnaordex  8612  php3  9181  frfi  9233  infglb  9439  suc11reg  9576  cardne  9939  cardsdomel  9948  carduni  9955  acndom  10023  alephinit  10067  cfflb  10231  cfslb2n  10240  fin23lem28  10312  isf34lem6  10352  fin1a2lem9  10380  axcc3  10410  winalim2  10669  inar1  10748  rankcf  10750  addclprlem2  10990  mulclprlem  10992  ltexprlem7  11015  prlem936  11020  reclem4pr  11023  sqgt0sr  11079  ltord2  11731  leord2  11732  eqord2  11733  mulge0b  12073  lt2halves  12467  addltmul  12468  ltsubnn0  12543  nzadd  12630  zextlt  12658  recnz  12659  zeo  12670  peano5uzi  12673  uzm1  12884  irradd  12985  irrmul  12986  xltneg  13231  xleadd1  13269  xmulasslem  13299  xlemul1a  13302  xlemul1  13304  fznuz  13625  uznfz  13626  axdc4uzlem  14007  facndiv  14312  hashvnfin  14384  hashgt12el  14447  hashgt12el2  14448  hashf1  14482  ccatalpha  14619  swrdccatin2  14754  swrdccatin2d  14769  rennim  15278  cau3lem  15394  caubnd2  15397  o1lo1  15576  climrlim2  15586  climshft  15615  subcn2  15634  mulcn2  15635  rlimo1  15656  o1dif  15669  isercoll  15707  caucvgrlem  15712  serf0  15720  cvgrat  15925  efieq1re  16243  moddvds  16309  dvdsssfz1  16364  smuval2  16528  nn0seqcvgd  16616  algcvgblem  16623  eucalglt  16631  lcmgcdlem  16652  rpmul  16705  divgcdcoprm0  16711  isprm6  16761  rpexp  16769  eulerthlem2  16829  prmdiv  16832  pcprendvds2  16889  pcz  16929  pcprmpw  16931  pcadd2  16938  pcfac  16947  expnprm  16950  ramlb  17067  firest  17473  joineu  18424  meeteu  18438  latjlej1  18497  latjlej2  18498  latmlem1  18513  latmlem2  18514  lubun  18559  acsmapd  18598  imasgrp2  19109  issubg4  19200  psgnunilem4  19555  oddvdsnn0  19602  odmulgeq  19615  subgpgp  19655  odcau  19662  lsmlub  19722  frgpnabllem1  19931  pgpfac1lem2  20135  pgpfac1lem3a  20136  pgpfac1lem3  20137  irredrmul  20497  isdomn4  20788  islmhm2  21125  lsmelval2  21172  lspsnat  21235  znidomb  21668  ip2eq  21760  lsmcss  21799  cnpnei  23378  cncls2  23387  cncls  23388  cnntr  23389  cnt0  23460  isnrm2  23472  comppfsc  23646  kqcldsat  23847  isr0  23851  hmeoopn  23880  hmeocld  23881  trufil  24024  opnsubg  24222  ghmcnp  24229  tgphaus  24231  qustgpopn  24234  tsmsgsum  24253  isngp4  24726  xrhmeo  25062  bndth  25074  cfilres  25412  caubl  25424  ivthlem2  25568  ovolicc2  25638  ismbf3d  25770  itg1ge0a  25827  mbfi1flim  25839  itg2gt0  25876  dvge0  26122  dvcnvrelem1  26133  dvcvx  26136  mdegmullem  26192  ig1peu  26289  plyco  26355  coemulc  26369  dgreq0  26379  dgrlt  26380  plymul0or  26396  plydiveu  26416  quotcan  26427  aalioulem3  26452  ulmcaulem  26511  sincosq3sgn  26619  sincosq4sgn  26620  sineq0  26643  logrec  26882  xrlimcnp  27087  cxploglim  27096  lgamgulmlem1  27147  mumul  27299  chtub  27330  perfect1  27346  dchrelbas3  27356  lgsdir2lem4  27446  lgsne0  27453  lgsquad2lem2  27503  2sqlem8a  27543  2sqblem  27549  nogt01o  27814  ltslpss  28055  ltadds2im  28133  ltnegs  28192  z12bday  28632  axcontlem2  29220  elntg2  29240  redwlklem  29924  redwlk  29925  crctcshwlkn0lem3  30066  crctcshwlkn0lem5  30068  clwwlkext2edg  30312  wwlksubclwwlk  30314  frgrwopregasn  30572  frgrwopregbsn  30573  blocnilem  31061  ip2eqi  31113  ubthlem2  31128  hial0  31359  hial02  31360  hial2eq  31363  h1datomi  31838  sumspansn  31906  lnopcnbd  32293  riesz4i  32320  bra11  32365  pjss2coi  32421  pjnormssi  32425  pjorthcoi  32426  pjclem4a  32455  pj3lem1  32463  pj3cor1i  32466  hst1h  32484  stm1i  32500  strlem1  32507  golem2  32529  mdbr2  32553  dmdbr5  32565  mdsl2i  32579  atexch  32638  atcvatlem  32642  chirredlem1  32647  cdjreui  32689  cdj1i  32690  cdj3lem1  32691  xraddge02  33010  submarchi  33414  isarchiofld  33427  esumcvg  34388  bnj1468  35146  loop1cycl  35495  erdsze2lem2  35562  btwnexch  36383  btwncolinear2  36428  btwncolinear3  36429  btwncolinear4  36430  btwncolinear5  36431  btwncolinear6  36432  nn0prpw  36691  cldbnd  36694  onsuct0  36809  onint1  36817  bj-ceqsalt0  37376  bj-ceqsalt1  37377  bj-inftyexpiinj  37708  bj-bary1lem1  37810  bj-bary1  37811  relowlssretop  37864  isinf2  37906  ltflcei  38114  tan2h  38118  poimirlem26  38152  poimirlem31  38157  ftc1anclem6  38204  dvasin  38210  dvacos  38211  fdc  38251  caushft  38267  heibor1lem  38315  bfplem2  38329  rrncmslem  38338  rngosn3  38430  mpobi123f  38668  riotasv3d  39591  lsatcv1  39679  lub0N  39820  glb0N  39824  oplecon3b  39831  cmtbr4N  39886  cvrnbtwn2  39906  atnlt  39944  atlatle  39951  cvlsupr2  39974  cvrexchlem  40050  cvratlem  40052  atcvrj0  40059  cvrat4  40074  cvrat42  40075  4noncolr3  40084  ps-1  40108  llnnlt  40154  lplnnlt  40196  lvolnltN  40249  dalempnes  40282  dalemqnet  40283  dalem-cly  40302  dalem44  40347  pmaple  40392  cdlemblem  40424  paddss  40476  2polcon4bN  40549  ltrneq2  40779  cdlemc3  40824  cdleme11h  40897  cdleme16b  40910  cdlemednpq  40930  tendospcanN  41654  dihmeetlem13N  41950  mapdordlem2  42268  mapdn0  42300  rspcsbnea  42755  ccatcan2d  42874  ctbnfien  43402  rmxypairf1o  43495  monotoddzzfi  43526  oddcomabszz  43528  acongtr  43562  onsupnmax  43812  onsupsucismax  43863  frege124d  44344  expgrowth  44904  sbcbi  45107  limsupmnflem  46293  funressnfv  47636  funfocofob  47671  2elfz2melfz  47911  iccpartnel  48043  requad2  48244  grlictr  48636  gpg5nbgrvtx13starlem1  48692  gpg5nbgrvtx13starlem3  48694  uzlidlring  48856  ply1mulgsumlem2  49019  fllog2  49200  dignn0flhalflem1  49247