Theorem sylibd 231

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  3imtr3d  285  ceqsalt  3442  sbceqal  3732  csbiebt  3802  rspcsbela  4265  sneqrg  4638  preq1b  4645  csbexg  5065  elrnrexdm  6674  isoselem  6911  riotass2  6958  ordzsl  7370  oaword2  7974  oaordex  7979  omword1  7994  om00  7996  omeulem2  8004  oen0  8007  oeeui  8023  nnaordex  8059  php3  8493  onomeneq  8497  frfi  8552  infglb  8743  suc11reg  8870  cardne  9182  cardsdomel  9191  carduni  9198  acndom  9265  alephinit  9309  cfflb  9473  cfslb2n  9482  fin23lem28  9554  isf34lem6  9594  fin1a2lem9  9622  axcc3  9652  winalim2  9910  inar1  9989  rankcf  9991  addclprlem2  10231  mulclprlem  10233  ltexprlem7  10256  prlem936  10261  reclem4pr  10264  sqgt0sr  10320  ltord2  10964  leord2  10965  eqord2  10966  mulgt1  11294  mulge0b  11305  fiminreOLD  11385  lt2halves  11676  addltmul  11677  ltsubnn0  11754  nzadd  11837  zextlt  11863  recnz  11864  zeo  11875  peano5uzi  11878  uzm1  12084  irradd  12181  irrmul  12182  xltneg  12421  xleadd1  12458  xmulasslem  12488  xlemul1a  12491  xlemul1  12493  fznuz  12799  uznfz  12800  axdc4uzlem  13160  facndiv  13457  hashvnfin  13530  hashgt12el  13590  hashgt12el2  13591  hashf1  13622  ccatalpha  13750  swrdccatin2  13923  swrdccatin2d  13946  swrdccatin12dOLD  13948  rennim  14453  cau3lem  14569  caubnd2  14572  o1lo1  14749  climrlim2  14759  climshft  14788  subcn2  14806  mulcn2  14807  rlimo1  14828  o1dif  14841  isercoll  14879  caucvgrlem  14884  serf0  14892  cvgrat  15093  efieq1re  15406  moddvds  15472  dvdsssfz1  15522  smuval2  15685  nn0seqcvgd  15764  algcvgblem  15771  eucalglt  15779  lcmgcdlem  15800  rpmul  15853  divgcdcoprm0  15859  isprm6  15908  rpexp  15914  eulerthlem2  15969  prmdiv  15972  pcprendvds2  16028  pcz  16067  pcprmpw  16069  pcadd2  16076  pcfac  16085  expnprm  16088  ramlb  16205  firest  16556  joineu  17472  meeteu  17486  latjlej1  17527  latjlej2  17528  latmlem1  17543  latmlem2  17544  lubun  17585  acsmapd  17640  imasgrp2  17995  issubg4  18076  psgnunilem4  18381  oddvdsnn0  18428  odmulgeq  18439  subgpgp  18477  odcau  18484  lsmlub  18543  frgpnabllem1  18743  pgpfac1lem2  18941  pgpfac1lem3a  18942  pgpfac1lem3  18943  irredrmul  19174  islmhm2  19526  lsmelval2  19573  lspsnat  19633  znidomb  20404  ip2eq  20493  lsmcss  20532  cnpnei  21570  cncls2  21579  cncls  21580  cnntr  21581  cnt0  21652  isnrm2  21664  comppfsc  21838  kqcldsat  22039  isr0  22043  hmeoopn  22072  hmeocld  22073  trufil  22216  opnsubg  22413  ghmcnp  22420  tgphaus  22422  qustgpopn  22425  tsmsgsum  22444  isngp4  22918  xrhmeo  23247  bndth  23259  cfilres  23596  caubl  23608  ivthlem2  23750  ovolicc2  23820  ismbf3d  23952  itg1ge0a  24009  mbfi1flim  24021  itg2gt0  24058  dvge0  24300  dvcnvrelem1  24311  dvcvx  24314  mdegmullem  24369  ig1peu  24462  plyco  24528  coemulc  24542  dgreq0  24552  dgrlt  24553  plymul0or  24567  plydiveu  24584  quotcan  24595  aalioulem3  24620  ulmcaulem  24679  sincosq3sgn  24783  sincosq4sgn  24784  sineq0  24806  logrec  25036  xrlimcnp  25242  cxploglim  25251  lgamgulmlem1  25302  mumul  25454  chtub  25484  perfect1  25500  dchrelbas3  25510  lgsdir2lem4  25600  lgsne0  25607  lgsquad2lem2  25657  2sqlem8a  25697  2sqblem  25703  axcontlem2  26448  elntg2  26468  redwlklem  27153  redwlk  27154  crctcshwlkn0lem3  27292  crctcshwlkn0lem5  27294  clwwlkext2edg  27573  wwlksubclwwlk  27575  wwlksubclwwlkOLD  27576  frgrwopregasn  27844  frgrwopregbsn  27845  blocnilem  28352  ip2eqi  28405  ubthlem2  28420  hial0  28652  hial02  28653  hial2eq  28656  h1datomi  29133  sumspansn  29201  lnopcnbd  29588  riesz4i  29615  bra11  29660  pjss2coi  29716  pjnormssi  29720  pjorthcoi  29721  pjclem4a  29750  pj3lem1  29758  pj3cor1i  29761  hst1h  29779  stm1i  29795  strlem1  29802  golem2  29824  mdbr2  29848  dmdbr5  29860  mdsl2i  29874  atexch  29933  atcvatlem  29937  chirredlem1  29942  cdjreui  29984  cdj1i  29985  cdj3lem1  29986  xraddge02  30233  submarchi  30481  isarchiofld  30569  esumcvg  30989  bnj1468  31765  erdsze2lem2  32036  funeldmb  32526  btwnexch  33007  btwncolinear2  33052  btwncolinear3  33053  btwncolinear4  33054  btwncolinear5  33055  btwncolinear6  33056  nn0prpw  33192  cldbnd  33195  onsuct0  33309  onint1  33317  bj-ceqsalt0  33693  bj-ceqsalt1  33694  bj-inftyexpiinj  33960  bj-bary1lem1  34040  bj-bary1  34041  relowlssretop  34086  isinf2  34127  ltflcei  34321  tan2h  34325  poimirlem26  34359  poimirlem31  34364  ftc1anclem6  34413  dvasin  34419  dvacos  34420  fdc  34462  caushft  34478  heibor1lem  34529  bfplem2  34543  rrncmslem  34552  rngosn3  34644  mpobi123f  34884  riotasv3d  35541  lsatcv1  35629  lub0N  35770  glb0N  35774  oplecon3b  35781  cmtbr4N  35836  cvrnbtwn2  35856  atnlt  35894  atlatle  35901  cvlsupr2  35924  cvrexchlem  36000  cvratlem  36002  atcvrj0  36009  cvrat4  36024  cvrat42  36025  4noncolr3  36034  ps-1  36058  llnnlt  36104  lplnnlt  36146  lvolnltN  36199  dalempnes  36232  dalemqnet  36233  dalem-cly  36252  dalem44  36297  pmaple  36342  cdlemblem  36374  paddss  36426  2polcon4bN  36499  ltrneq2  36729  cdlemc3  36774  cdleme11h  36847  cdleme16b  36860  cdlemednpq  36880  tendospcanN  37604  dihmeetlem13N  37900  mapdordlem2  38218  mapdn0  38250  ccatcan2d  38572  ctbnfien  38811  rmxypairf1o  38904  monotoddzzfi  38935  oddcomabszz  38937  acongtr  38971  frege124d  39469  expgrowth  40083  sbcbi  40292  limsupmnflem  41432  funressnfv  42683  2elfz2melfz  42924  iccpartnel  42970  requad2  43156  uzlidlring  43564  ply1mulgsumlem2  43808  fllog2  43996  dignn0flhalflem1  44043