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  csbiebt  3894  rspcsbela  4404  sneqrg  4806  preq1b  4813  csbexg  5268  elrnrexdm  7064  isoselem  7319  funeldmb  7337  riotass2  7377  ordzsl  7824  resf1extb  7913  oaword2  8520  oaordex  8525  omword1  8540  om00  8542  omeulem2  8550  oen0  8553  oeeui  8569  nnaordex  8605  php3  9179  frfi  9239  infglb  9449  suc11reg  9579  cardne  9925  cardsdomel  9934  carduni  9941  acndom  10011  alephinit  10055  cfflb  10219  cfslb2n  10228  fin23lem28  10300  isf34lem6  10340  fin1a2lem9  10368  axcc3  10398  winalim2  10656  inar1  10735  rankcf  10737  addclprlem2  10977  mulclprlem  10979  ltexprlem7  11002  prlem936  11007  reclem4pr  11010  sqgt0sr  11066  ltord2  11714  leord2  11715  eqord2  11716  mulgt1OLD  12048  mulge0b  12060  lt2halves  12424  addltmul  12425  ltsubnn0  12500  nzadd  12588  zextlt  12615  recnz  12616  zeo  12627  peano5uzi  12630  uzm1  12838  irradd  12939  irrmul  12940  xltneg  13184  xleadd1  13222  xmulasslem  13252  xlemul1a  13255  xlemul1  13257  fznuz  13577  uznfz  13578  axdc4uzlem  13955  facndiv  14260  hashvnfin  14332  hashgt12el  14394  hashgt12el2  14395  hashf1  14429  ccatalpha  14565  swrdccatin2  14701  swrdccatin2d  14716  rennim  15212  cau3lem  15328  caubnd2  15331  o1lo1  15510  climrlim2  15520  climshft  15549  subcn2  15568  mulcn2  15569  rlimo1  15590  o1dif  15603  isercoll  15641  caucvgrlem  15646  serf0  15654  cvgrat  15856  efieq1re  16174  moddvds  16240  dvdsssfz1  16295  smuval2  16459  nn0seqcvgd  16547  algcvgblem  16554  eucalglt  16562  lcmgcdlem  16583  rpmul  16636  divgcdcoprm0  16642  isprm6  16691  rpexp  16699  eulerthlem2  16759  prmdiv  16762  pcprendvds2  16819  pcz  16859  pcprmpw  16861  pcadd2  16868  pcfac  16877  expnprm  16880  ramlb  16997  firest  17402  joineu  18348  meeteu  18362  latjlej1  18419  latjlej2  18420  latmlem1  18435  latmlem2  18436  lubun  18481  acsmapd  18520  imasgrp2  18994  issubg4  19084  psgnunilem4  19434  oddvdsnn0  19481  odmulgeq  19494  subgpgp  19534  odcau  19541  lsmlub  19601  frgpnabllem1  19810  pgpfac1lem2  20014  pgpfac1lem3a  20015  pgpfac1lem3  20016  irredrmul  20343  isdomn4  20632  islmhm2  20952  lsmelval2  20999  lspsnat  21062  znidomb  21478  ip2eq  21569  lsmcss  21608  cnpnei  23158  cncls2  23167  cncls  23168  cnntr  23169  cnt0  23240  isnrm2  23252  comppfsc  23426  kqcldsat  23627  isr0  23631  hmeoopn  23660  hmeocld  23661  trufil  23804  opnsubg  24002  ghmcnp  24009  tgphaus  24011  qustgpopn  24014  tsmsgsum  24033  isngp4  24507  xrhmeo  24851  bndth  24864  cfilres  25203  caubl  25215  ivthlem2  25360  ovolicc2  25430  ismbf3d  25562  itg1ge0a  25619  mbfi1flim  25631  itg2gt0  25668  dvge0  25918  dvcnvrelem1  25929  dvcvx  25932  mdegmullem  25990  ig1peu  26087  plyco  26153  coemulc  26167  dgreq0  26178  dgrlt  26179  plymul0or  26195  plydiveu  26213  quotcan  26224  aalioulem3  26249  ulmcaulem  26310  sincosq3sgn  26416  sincosq4sgn  26417  sineq0  26440  logrec  26680  xrlimcnp  26885  cxploglim  26895  lgamgulmlem1  26946  mumul  27098  chtub  27130  perfect1  27146  dchrelbas3  27156  lgsdir2lem4  27246  lgsne0  27253  lgsquad2lem2  27303  2sqlem8a  27343  2sqblem  27349  nogt01o  27615  sltlpss  27826  sltadd2im  27900  sltneg  27958  axcontlem2  28899  elntg2  28919  redwlklem  29606  redwlk  29607  crctcshwlkn0lem3  29749  crctcshwlkn0lem5  29751  clwwlkext2edg  29992  wwlksubclwwlk  29994  frgrwopregasn  30252  frgrwopregbsn  30253  blocnilem  30740  ip2eqi  30792  ubthlem2  30807  hial0  31038  hial02  31039  hial2eq  31042  h1datomi  31517  sumspansn  31585  lnopcnbd  31972  riesz4i  31999  bra11  32044  pjss2coi  32100  pjnormssi  32104  pjorthcoi  32105  pjclem4a  32134  pj3lem1  32142  pj3cor1i  32145  hst1h  32163  stm1i  32179  strlem1  32186  golem2  32208  mdbr2  32232  dmdbr5  32244  mdsl2i  32258  atexch  32317  atcvatlem  32321  chirredlem1  32326  cdjreui  32368  cdj1i  32369  cdj3lem1  32370  xraddge02  32687  submarchi  33147  isarchiofld  33302  esumcvg  34083  bnj1468  34843  loop1cycl  35131  erdsze2lem2  35198  btwnexch  36020  btwncolinear2  36065  btwncolinear3  36066  btwncolinear4  36067  btwncolinear5  36068  btwncolinear6  36069  nn0prpw  36318  cldbnd  36321  onsuct0  36436  onint1  36444  bj-ceqsalt0  36879  bj-ceqsalt1  36880  bj-inftyexpiinj  37204  bj-bary1lem1  37306  bj-bary1  37307  relowlssretop  37358  isinf2  37400  ltflcei  37609  tan2h  37613  poimirlem26  37647  poimirlem31  37652  ftc1anclem6  37699  dvasin  37705  dvacos  37706  fdc  37746  caushft  37762  heibor1lem  37810  bfplem2  37824  rrncmslem  37833  rngosn3  37925  mpobi123f  38163  riotasv3d  38960  lsatcv1  39048  lub0N  39189  glb0N  39193  oplecon3b  39200  cmtbr4N  39255  cvrnbtwn2  39275  atnlt  39313  atlatle  39320  cvlsupr2  39343  cvrexchlem  39420  cvratlem  39422  atcvrj0  39429  cvrat4  39444  cvrat42  39445  4noncolr3  39454  ps-1  39478  llnnlt  39524  lplnnlt  39566  lvolnltN  39619  dalempnes  39652  dalemqnet  39653  dalem-cly  39672  dalem44  39717  pmaple  39762  cdlemblem  39794  paddss  39846  2polcon4bN  39919  ltrneq2  40149  cdlemc3  40194  cdleme11h  40267  cdleme16b  40280  cdlemednpq  40300  tendospcanN  41024  dihmeetlem13N  41320  mapdordlem2  41638  mapdn0  41670  rspcsbnea  42126  ccatcan2d  42246  ctbnfien  42813  rmxypairf1o  42907  monotoddzzfi  42938  oddcomabszz  42940  acongtr  42974  onsupnmax  43224  onsupsucismax  43275  frege124d  43757  expgrowth  44331  sbcbi  44536  limsupmnflem  45725  funressnfv  47048  funfocofob  47083  2elfz2melfz  47323  iccpartnel  47443  requad2  47628  grlictr  48011  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem3  48068  uzlidlring  48227  ply1mulgsumlem2  48380  fllog2  48561  dignn0flhalflem1  48608