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  3883  rspcsbela  4404  sneqrg  4805  preq1b  4812  csbexg  5274  elrnrexdm  7086  isoselem  7341  funeldmb  7359  riotass2  7399  ordzsl  7842  resf1extb  7932  oaword2  8539  oaordex  8544  omword1  8559  om00  8561  omeulem2  8569  oen0  8573  oeeui  8589  nnaordex  8625  php3  9194  frfi  9246  infglb  9452  suc11reg  9589  cardne  9952  cardsdomel  9961  carduni  9968  acndom  10036  alephinit  10080  cfflb  10244  cfslb2n  10253  fin23lem28  10325  isf34lem6  10365  fin1a2lem9  10393  axcc3  10423  winalim2  10682  inar1  10761  rankcf  10763  addclprlem2  11003  mulclprlem  11005  ltexprlem7  11028  prlem936  11033  reclem4pr  11036  sqgt0sr  11092  ltord2  11744  leord2  11745  eqord2  11746  mulge0b  12086  lt2halves  12480  addltmul  12481  ltsubnn0  12556  nzadd  12643  zextlt  12671  recnz  12672  zeo  12683  peano5uzi  12686  uzm1  12897  irradd  12998  irrmul  12999  xltneg  13244  xleadd1  13282  xmulasslem  13312  xlemul1a  13315  xlemul1  13317  fznuz  13639  uznfz  13640  axdc4uzlem  14021  facndiv  14326  hashvnfin  14398  hashgt12el  14461  hashgt12el2  14462  hashf1  14496  ccatalpha  14633  swrdccatin2  14768  swrdccatin2d  14783  rennim  15292  cau3lem  15408  caubnd2  15411  o1lo1  15590  climrlim2  15600  climshft  15629  subcn2  15648  mulcn2  15649  rlimo1  15670  o1dif  15683  isercoll  15721  caucvgrlem  15726  serf0  15734  cvgrat  15939  efieq1re  16256  moddvds  16322  dvdsssfz1  16377  smuval2  16541  nn0seqcvgd  16629  algcvgblem  16636  eucalglt  16644  lcmgcdlem  16665  rpmul  16718  divgcdcoprm0  16724  isprm6  16774  rpexp  16782  eulerthlem2  16842  prmdiv  16845  pcprendvds2  16902  pcz  16942  pcprmpw  16944  pcadd2  16951  pcfac  16960  expnprm  16963  ramlb  17080  firest  17486  joineu  18437  meeteu  18451  latjlej1  18510  latjlej2  18511  latmlem1  18526  latmlem2  18527  lubun  18572  acsmapd  18611  imasgrp2  19122  issubg4  19213  psgnunilem4  19568  oddvdsnn0  19615  odmulgeq  19628  subgpgp  19668  odcau  19675  lsmlub  19735  frgpnabllem1  19944  pgpfac1lem2  20148  pgpfac1lem3a  20149  pgpfac1lem3  20150  irredrmul  20510  isdomn4  20801  islmhm2  21140  lsmelval2  21187  lspsnat  21250  znidomb  21692  ip2eq  21784  lsmcss  21823  cnpnei  23402  cncls2  23411  cncls  23412  cnntr  23413  cnt0  23484  isnrm2  23496  comppfsc  23670  kqcldsat  23871  isr0  23875  hmeoopn  23904  hmeocld  23905  trufil  24048  opnsubg  24246  ghmcnp  24253  tgphaus  24255  qustgpopn  24258  tsmsgsum  24277  isngp4  24750  xrhmeo  25086  bndth  25098  cfilres  25436  caubl  25448  ivthlem2  25592  ovolicc2  25662  ismbf3d  25794  itg1ge0a  25851  mbfi1flim  25863  itg2gt0  25900  dvge0  26146  dvcnvrelem1  26157  dvcvx  26160  mdegmullem  26216  ig1peu  26313  plyco  26379  coemulc  26393  dgreq0  26403  dgrlt  26404  plymul0or  26420  plydiveu  26440  quotcan  26451  aalioulem3  26476  ulmcaulem  26535  sincosq3sgn  26643  sincosq4sgn  26644  sineq0  26667  logrec  26906  xrlimcnp  27111  cxploglim  27120  lgamgulmlem1  27171  mumul  27323  chtub  27354  perfect1  27370  dchrelbas3  27380  lgsdir2lem4  27470  lgsne0  27477  lgsquad2lem2  27527  2sqlem8a  27567  2sqblem  27573  nogt01o  27838  ltslpss  28079  ltadds2im  28157  ltnegs  28216  z12bday  28656  axcontlem2  29293  elntg2  29313  redwlklem  29997  redwlk  29998  crctcshwlkn0lem3  30139  crctcshwlkn0lem5  30141  clwwlkext2edg  30385  wwlksubclwwlk  30387  frgrwopregasn  30645  frgrwopregbsn  30646  blocnilem  31134  ip2eqi  31186  ubthlem2  31201  hial0  31432  hial02  31433  hial2eq  31436  h1datomi  31911  sumspansn  31979  lnopcnbd  32366  riesz4i  32393  bra11  32438  pjss2coi  32494  pjnormssi  32498  pjorthcoi  32499  pjclem4a  32528  pj3lem1  32536  pj3cor1i  32539  hst1h  32557  stm1i  32573  strlem1  32580  golem2  32602  mdbr2  32626  dmdbr5  32638  mdsl2i  32652  atexch  32711  atcvatlem  32715  chirredlem1  32720  cdjreui  32762  cdj1i  32763  cdj3lem1  32764  xraddge02  33080  submarchi  33484  isarchiofld  33497  esumcvg  34454  bnj1468  35212  loop1cycl  35607  erdsze2lem2  35674  btwnexch  36495  btwncolinear2  36540  btwncolinear3  36541  btwncolinear4  36542  btwncolinear5  36543  btwncolinear6  36544  nn0prpw  36812  cldbnd  36815  onsuct0  36930  onint1  36938  bj-ceqsalt0  37497  bj-ceqsalt1  37498  bj-inftyexpiinj  37831  bj-bary1lem1  37933  bj-bary1  37934  relowlssretop  37987  isinf2  38029  ltflcei  38237  tan2h  38241  poimirlem26  38275  poimirlem31  38280  ftc1anclem6  38327  dvasin  38333  dvacos  38334  fdc  38374  caushft  38390  heibor1lem  38438  bfplem2  38452  rrncmslem  38461  rngosn3  38553  mpobi123f  38789  riotasv3d  39712  lsatcv1  39800  lub0N  39941  glb0N  39945  oplecon3b  39952  cmtbr4N  40007  cvrnbtwn2  40027  atnlt  40065  atlatle  40072  cvlsupr2  40095  cvrexchlem  40171  cvratlem  40173  atcvrj0  40180  cvrat4  40195  cvrat42  40196  4noncolr3  40205  ps-1  40229  llnnlt  40275  lplnnlt  40317  lvolnltN  40370  dalempnes  40403  dalemqnet  40404  dalem-cly  40423  dalem44  40468  pmaple  40513  cdlemblem  40545  paddss  40597  2polcon4bN  40670  ltrneq2  40900  cdlemc3  40945  cdleme11h  41018  cdleme16b  41031  cdlemednpq  41051  tendospcanN  41775  dihmeetlem13N  42071  mapdordlem2  42389  mapdn0  42421  rspcsbnea  42876  ccatcan2d  42997  ctbnfien  43525  rmxypairf1o  43618  monotoddzzfi  43649  oddcomabszz  43651  acongtr  43685  onsupnmax  43935  onsupsucismax  43986  frege124d  44467  expgrowth  45025  sbcbi  45228  limsupmnflem  46414  funressnfv  47757  funfocofob  47792  2elfz2melfz  48032  iccpartnel  48164  requad2  48365  grlictr  48757  gpg5nbgrvtx13starlem1  48813  gpg5nbgrvtx13starlem3  48815  uzlidlring  48977  ply1mulgsumlem2  49144  fllog2  49325  dignn0flhalflem1  49372