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 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3imtr3d  296  csbiebt  3876  rspcsbela  4396  sneqrg  4799  preq1b  4806  csbexg  5264  elrnrexdm  7081  isoselem  7341  funeldmb  7361  riotass2  7399  ordzsl  7845  resf1extb  7935  oaword2  8545  oaordex  8550  omword1  8565  om00  8567  omeulem2  8575  oen0  8579  oeeui  8595  nnaordex  8631  php3  9208  frfi  9260  infglb  9467  suc11reg  9604  cardne  10027  cardsdomel  10036  carduni  10043  acndom  10111  alephinit  10155  cfflb  10318  cfslb2n  10327  fin23lem28  10399  isf34lem6  10439  fin1a2lem9  10467  axcc3  10497  winalim2  10762  inar1  10841  rankcf  10843  addclprlem2  11083  mulclprlem  11085  ltexprlem7  11108  prlem936  11113  reclem4pr  11116  sqgt0sr  11172  ltord2  11826  leord2  11827  eqord2  11828  mulge0b  12168  lt2halves  12562  addltmul  12563  ltsubnn0  12638  nzadd  12725  zextlt  12754  recnz  12755  zeo  12766  peano5uzi  12769  uzm1  12980  irradd  13082  irrmul  13083  xltneg  13328  xleadd1  13366  xmulasslem  13396  xlemul1a  13399  xlemul1  13401  fznuz  13723  uznfz  13724  axdc4uzlem  14106  facndiv  14412  hashvnfin  14484  hashgt12el  14547  hashgt12el2  14548  hashf1  14582  ccatalpha  14720  swrdccatin2  14858  swrdccatin2d  14873  rennim  15386  cau3lem  15502  caubnd2  15505  o1lo1  15684  climrlim2  15694  climshft  15723  subcn2  15742  mulcn2  15743  rlimo1  15764  o1dif  15777  isercoll  15815  caucvgrlem  15820  serf0  15828  cvgrat  16032  efieq1re  16347  moddvds  16413  dvdsssfz1  16468  smuval2  16632  nn0seqcvgd  16725  algcvgblem  16732  eucalglt  16740  lcmgcdlem  16761  rpmul  16814  divgcdcoprm0  16820  isprm6  16870  rpexp  16878  eulerthlem2  16939  prmdiv  16942  pcprendvds2  16999  pcz  17039  pcprmpw  17041  pcadd2  17048  pcfac  17057  expnprm  17060  ramlb  17177  firest  17583  joineu  18534  meeteu  18548  latjlej1  18607  latjlej2  18608  latmlem1  18623  latmlem2  18624  lubun  18669  acsmapd  18708  idressid  18842  imasgrp2  19245  issubg4  19336  psgnunilem4  19691  oddvdsnn0  19738  odmulgeq  19751  subgpgp  19791  odcau  19798  lsmlub  19858  frgpnabllem1  20067  pgpfac1lem2  20271  pgpfac1lem3a  20272  pgpfac1lem3  20273  irredrmul  20637  isdomn4  20947  islmhm2  21293  lsmelval2  21340  lspsnat  21403  znidomb  21847  ip2eq  21939  lsmcss  21978  cnpnei  23562  cncls2  23571  cncls  23572  cnntr  23573  cnt0  23644  isnrm2  23656  comppfsc  23831  kqcldsat  24032  isr0  24036  hmeoopn  24065  hmeocld  24066  trufil  24209  opnsubg  24407  ghmcnp  24414  tgphaus  24416  qustgpopn  24419  tsmsgsum  24438  isngp4  24911  xrhmeo  25247  bndth  25259  cfilres  25597  caubl  25609  ivthlem2  25753  ovolicc2  25823  ismbf3d  25955  itg1ge0a  26012  mbfi1flim  26024  itg2gt0  26061  dvge0  26306  dvcnvrelem1  26317  dvcvx  26320  mdegmullem  26376  ig1peu  26473  plyco  26540  coemulc  26554  dgreq0  26564  dgrlt  26565  plymul0or  26581  plydiveu  26601  quotcan  26614  aalioulem3  26643  ulmcaulem  26703  sincosq3sgn  26811  sincosq4sgn  26812  sineq0  26834  logrec  27073  xrlimcnp  27278  cxploglim  27287  lgamgulmlem1  27338  mumul  27490  chtub  27521  perfect1  27537  dchrelbas3  27547  lgsdir2lem4  27637  lgsne0  27644  lgsquad2lem2  27694  2sqlem8a  27734  2sqblem  27740  nogt01o  28035  ltslpss  28276  ltadds2im  28354  ltnegs  28413  z12bday  28853  axcontlem2  29525  elntg2  29545  redwlklem  30232  redwlk  30233  crctcshwlkn0lem3  30383  crctcshwlkn0lem5  30385  clwwlkext2edg  30629  wwlksubclwwlk  30631  loop1cycl  30726  frgrwopregasn  30899  frgrwopregbsn  30900  blocnilem  31388  ip2eqi  31440  ubthlem2  31455  hial0  31686  hial02  31687  hial2eq  31690  h1datomi  32165  sumspansn  32233  lnopcnbd  32620  riesz4i  32647  bra11  32692  pjss2coi  32748  pjnormssi  32752  pjorthcoi  32753  pjclem4a  32782  pj3lem1  32790  pj3cor1i  32793  hst1h  32811  stm1i  32827  strlem1  32834  golem2  32856  mdbr2  32880  dmdbr5  32892  mdsl2i  32906  atexch  32965  atcvatlem  32969  chirredlem1  32974  cdjreui  33016  cdj1i  33017  cdj3lem1  33018  xraddge02  33331  submarchi  33729  isarchiofld  33742  esumcvg  34700  bnj1468  35459  erdsze2lem2  35938  btwnexch  36760  btwncolinear2  36805  btwncolinear3  36806  btwncolinear4  36807  btwncolinear5  36808  btwncolinear6  36809  nn0prpw  37081  cldbnd  37084  onsuct0  37199  onint1  37207  bj-ceqsalt0  37766  bj-ceqsalt1  37767  bj-inftyexpiinj  38098  bj-bary1lem1  38200  bj-bary1  38201  relowlssretop  38254  isinf2  38296  ltflcei  38499  tan2h  38503  poimirlem26  38532  poimirlem31  38537  ftc1anclem6  38584  dvasin  38590  dvacos  38591  fdc  38647  caushft  38663  heibor1lem  38711  bfplem2  38725  rrncmslem  38734  rngosn3  38826  mpobi123f  39062  riotasv3d  39985  lsatcv1  40073  lub0N  40214  glb0N  40218  oplecon3b  40225  cmtbr4N  40280  cvrnbtwn2  40300  atnlt  40338  atlatle  40345  cvlsupr2  40368  cvrexchlem  40444  cvratlem  40446  atcvrj0  40453  cvrat4  40468  cvrat42  40469  4noncolr3  40478  ps-1  40502  llnnlt  40548  lplnnlt  40590  lvolnltN  40643  dalempnes  40676  dalemqnet  40677  dalem-cly  40696  dalem44  40741  pmaple  40786  cdlemblem  40818  paddss  40870  2polcon4bN  40943  ltrneq2  41173  cdlemc3  41218  cdleme11h  41291  cdleme16b  41304  cdlemednpq  41324  tendospcanN  42048  dihmeetlem13N  42344  mapdordlem2  42662  mapdn0  42694  rspcsbnea  43149  ccatcan2d  43270  ctbnfien  43778  rmxypairf1o  43871  monotoddzzfi  43902  oddcomabszz  43904  acongtr  43938  onsupnmax  44188  onsupsucismax  44239  frege124d  44720  expgrowth  45278  sbcbi  45481  limsupmnflem  46674  funressnfv  48057  funfocofob  48092  2elfz2melfz  48332  iccpartnel  48464  requad2  48665  grlictr  49057  gpg5nbgrvtx13starlem1  49113  gpg5nbgrvtx13starlem3  49115  uzlidlring  49276  ply1mulgsumlem2  49443  fllog2  49624  dignn0flhalflem1  49671