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  7090  isoselem  7341  funeldmb  7359  riotass2  7399  ordzsl  7838  oaword2  8559  oaordex  8564  omword1  8579  om00  8581  omeulem2  8589  oen0  8592  oeeui  8608  nnaordex  8644  php3  9218  php3OLD  9230  onomeneqOLD  9235  frfi  9294  infglb  9491  suc11reg  9620  cardne  9966  cardsdomel  9975  carduni  9982  acndom  10052  alephinit  10096  cfflb  10260  cfslb2n  10269  fin23lem28  10341  isf34lem6  10381  fin1a2lem9  10409  axcc3  10439  winalim2  10697  inar1  10776  rankcf  10778  addclprlem2  11018  mulclprlem  11020  ltexprlem7  11043  prlem936  11048  reclem4pr  11051  sqgt0sr  11107  ltord2  11750  leord2  11751  eqord2  11752  mulgt1  12080  mulge0b  12091  lt2halves  12454  addltmul  12455  ltsubnn0  12530  nzadd  12617  zextlt  12643  recnz  12644  zeo  12655  peano5uzi  12658  uzm1  12867  irradd  12964  irrmul  12965  xltneg  13203  xleadd1  13241  xmulasslem  13271  xlemul1a  13274  xlemul1  13276  fznuz  13590  uznfz  13591  axdc4uzlem  13955  facndiv  14255  hashvnfin  14327  hashgt12el  14389  hashgt12el2  14390  hashf1  14425  ccatalpha  14550  swrdccatin2  14686  swrdccatin2d  14701  rennim  15193  cau3lem  15308  caubnd2  15311  o1lo1  15488  climrlim2  15498  climshft  15527  subcn2  15546  mulcn2  15547  rlimo1  15568  o1dif  15581  isercoll  15621  caucvgrlem  15626  serf0  15634  cvgrat  15836  efieq1re  16149  moddvds  16215  dvdsssfz1  16268  smuval2  16430  nn0seqcvgd  16514  algcvgblem  16521  eucalglt  16529  lcmgcdlem  16550  rpmul  16603  divgcdcoprm0  16609  isprm6  16658  rpexp  16666  eulerthlem2  16722  prmdiv  16725  pcprendvds2  16781  pcz  16821  pcprmpw  16823  pcadd2  16830  pcfac  16839  expnprm  16842  ramlb  16959  firest  17385  joineu  18345  meeteu  18359  latjlej1  18416  latjlej2  18417  latmlem1  18432  latmlem2  18433  lubun  18478  acsmapd  18517  imasgrp2  18981  issubg4  19068  psgnunilem4  19413  oddvdsnn0  19460  odmulgeq  19473  subgpgp  19513  odcau  19520  lsmlub  19580  frgpnabllem1  19789  pgpfac1lem2  19993  pgpfac1lem3a  19994  pgpfac1lem3  19995  irredrmul  20325  islmhm2  20882  lsmelval2  20929  lspsnat  20992  isdomn4  21207  znidomb  21427  ip2eq  21516  lsmcss  21555  cnpnei  23088  cncls2  23097  cncls  23098  cnntr  23099  cnt0  23170  isnrm2  23182  comppfsc  23356  kqcldsat  23557  isr0  23561  hmeoopn  23590  hmeocld  23591  trufil  23734  opnsubg  23932  ghmcnp  23939  tgphaus  23941  qustgpopn  23944  tsmsgsum  23963  isngp4  24441  xrhmeo  24791  bndth  24804  cfilres  25144  caubl  25156  ivthlem2  25301  ovolicc2  25371  ismbf3d  25503  itg1ge0a  25561  mbfi1flim  25573  itg2gt0  25610  dvge0  25859  dvcnvrelem1  25870  dvcvx  25873  mdegmullem  25934  ig1peu  26027  plyco  26093  coemulc  26107  dgreq0  26118  dgrlt  26119  plymul0or  26133  plydiveu  26150  quotcan  26161  aalioulem3  26186  ulmcaulem  26245  sincosq3sgn  26350  sincosq4sgn  26351  sineq0  26373  logrec  26609  xrlimcnp  26814  cxploglim  26823  lgamgulmlem1  26874  mumul  27026  chtub  27058  perfect1  27074  dchrelbas3  27084  lgsdir2lem4  27174  lgsne0  27181  lgsquad2lem2  27231  2sqlem8a  27271  2sqblem  27277  nogt01o  27542  sltlpss  27746  sltadd2im  27816  sltneg  27870  axcontlem2  28656  elntg2  28676  redwlklem  29361  redwlk  29362  crctcshwlkn0lem3  29499  crctcshwlkn0lem5  29501  clwwlkext2edg  29742  wwlksubclwwlk  29744  frgrwopregasn  30002  frgrwopregbsn  30003  blocnilem  30490  ip2eqi  30542  ubthlem2  30557  hial0  30788  hial02  30789  hial2eq  30792  h1datomi  31267  sumspansn  31335  lnopcnbd  31722  riesz4i  31749  bra11  31794  pjss2coi  31850  pjnormssi  31854  pjorthcoi  31855  pjclem4a  31884  pj3lem1  31892  pj3cor1i  31895  hst1h  31913  stm1i  31929  strlem1  31936  golem2  31958  mdbr2  31982  dmdbr5  31994  mdsl2i  32008  atexch  32067  atcvatlem  32071  chirredlem1  32076  cdjreui  32118  cdj1i  32119  cdj3lem1  32120  xraddge02  32402  submarchi  32768  isarchiofld  32871  esumcvg  33548  bnj1468  34321  loop1cycl  34592  erdsze2lem2  34659  btwnexch  35467  btwncolinear2  35512  btwncolinear3  35513  btwncolinear4  35514  btwncolinear5  35515  btwncolinear6  35516  nn0prpw  35672  cldbnd  35675  onsuct0  35790  onint1  35798  bj-ceqsalt0  36228  bj-ceqsalt1  36229  bj-inftyexpiinj  36554  bj-bary1lem1  36656  bj-bary1  36657  relowlssretop  36708  isinf2  36750  ltflcei  36940  tan2h  36944  poimirlem26  36978  poimirlem31  36983  ftc1anclem6  37030  dvasin  37036  dvacos  37037  fdc  37077  caushft  37093  heibor1lem  37141  bfplem2  37155  rrncmslem  37164  rngosn3  37256  mpobi123f  37494  riotasv3d  38294  lsatcv1  38382  lub0N  38523  glb0N  38527  oplecon3b  38534  cmtbr4N  38589  cvrnbtwn2  38609  atnlt  38647  atlatle  38654  cvlsupr2  38677  cvrexchlem  38754  cvratlem  38756  atcvrj0  38763  cvrat4  38778  cvrat42  38779  4noncolr3  38788  ps-1  38812  llnnlt  38858  lplnnlt  38900  lvolnltN  38953  dalempnes  38986  dalemqnet  38987  dalem-cly  39006  dalem44  39051  pmaple  39096  cdlemblem  39128  paddss  39180  2polcon4bN  39253  ltrneq2  39483  cdlemc3  39528  cdleme11h  39601  cdleme16b  39614  cdlemednpq  39634  tendospcanN  40358  dihmeetlem13N  40654  mapdordlem2  40972  mapdn0  41004  ccatcan2d  41536  ctbnfien  42019  rmxypairf1o  42113  monotoddzzfi  42144  oddcomabszz  42146  acongtr  42180  onsupnmax  42440  onsupsucismax  42492  frege124d  42975  expgrowth  43557  sbcbi  43763  limsupmnflem  44895  funressnfv  46212  funfocofob  46245  2elfz2melfz  46485  iccpartnel  46565  requad2  46750  uzlidlring  47072  ply1mulgsumlem2  47230  fllog2  47416  dignn0flhalflem1  47463