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  3879  rspcsbela  4399  sneqrg  4802  preq1b  4809  csbexg  5271  elrnrexdm  7086  isoselem  7346  funeldmb  7366  riotass2  7404  ordzsl  7845  resf1extb  7935  oaword2  8544  oaordex  8549  omword1  8564  om00  8566  omeulem2  8574  oen0  8578  oeeui  8594  nnaordex  8630  php3  9207  frfi  9259  infglb  9465  suc11reg  9602  cardne  9974  cardsdomel  9983  carduni  9990  acndom  10058  alephinit  10102  cfflb  10265  cfslb2n  10274  fin23lem28  10346  isf34lem6  10386  fin1a2lem9  10414  axcc3  10444  winalim2  10709  inar1  10788  rankcf  10790  addclprlem2  11030  mulclprlem  11032  ltexprlem7  11055  prlem936  11060  reclem4pr  11063  sqgt0sr  11119  ltord2  11771  leord2  11772  eqord2  11773  mulge0b  12113  lt2halves  12507  addltmul  12508  ltsubnn0  12583  nzadd  12670  zextlt  12699  recnz  12700  zeo  12711  peano5uzi  12714  uzm1  12925  irradd  13027  irrmul  13028  xltneg  13273  xleadd1  13311  xmulasslem  13341  xlemul1a  13344  xlemul1  13346  fznuz  13668  uznfz  13669  axdc4uzlem  14051  facndiv  14356  hashvnfin  14428  hashgt12el  14491  hashgt12el2  14492  hashf1  14526  ccatalpha  14664  swrdccatin2  14802  swrdccatin2d  14817  rennim  15330  cau3lem  15446  caubnd2  15449  o1lo1  15628  climrlim2  15638  climshft  15667  subcn2  15686  mulcn2  15687  rlimo1  15708  o1dif  15721  isercoll  15759  caucvgrlem  15764  serf0  15772  cvgrat  15976  efieq1re  16293  moddvds  16359  dvdsssfz1  16414  smuval2  16578  nn0seqcvgd  16666  algcvgblem  16673  eucalglt  16681  lcmgcdlem  16702  rpmul  16755  divgcdcoprm0  16761  isprm6  16811  rpexp  16819  eulerthlem2  16879  prmdiv  16882  pcprendvds2  16939  pcz  16979  pcprmpw  16981  pcadd2  16988  pcfac  16997  expnprm  17000  ramlb  17117  firest  17523  joineu  18474  meeteu  18488  latjlej1  18547  latjlej2  18548  latmlem1  18563  latmlem2  18564  lubun  18609  acsmapd  18648  idressid  18781  imasgrp2  19184  issubg4  19275  psgnunilem4  19630  oddvdsnn0  19677  odmulgeq  19690  subgpgp  19730  odcau  19737  lsmlub  19797  frgpnabllem1  20006  pgpfac1lem2  20210  pgpfac1lem3a  20211  pgpfac1lem3  20212  irredrmul  20574  isdomn4  20883  islmhm2  21228  lsmelval2  21275  lspsnat  21338  znidomb  21780  ip2eq  21872  lsmcss  21911  cnpnei  23495  cncls2  23504  cncls  23505  cnntr  23506  cnt0  23577  isnrm2  23589  comppfsc  23764  kqcldsat  23965  isr0  23969  hmeoopn  23998  hmeocld  23999  trufil  24142  opnsubg  24340  ghmcnp  24347  tgphaus  24349  qustgpopn  24352  tsmsgsum  24371  isngp4  24844  xrhmeo  25180  bndth  25192  cfilres  25530  caubl  25542  ivthlem2  25686  ovolicc2  25756  ismbf3d  25888  itg1ge0a  25945  mbfi1flim  25957  itg2gt0  25994  dvge0  26240  dvcnvrelem1  26251  dvcvx  26254  mdegmullem  26310  ig1peu  26407  plyco  26474  coemulc  26488  dgreq0  26498  dgrlt  26499  plymul0or  26515  plydiveu  26535  quotcan  26548  aalioulem3  26577  ulmcaulem  26637  sincosq3sgn  26745  sincosq4sgn  26746  sineq0  26769  logrec  27008  xrlimcnp  27213  cxploglim  27222  lgamgulmlem1  27273  mumul  27425  chtub  27456  perfect1  27472  dchrelbas3  27482  lgsdir2lem4  27572  lgsne0  27579  lgsquad2lem2  27629  2sqlem8a  27669  2sqblem  27675  nogt01o  27940  ltslpss  28181  ltadds2im  28259  ltnegs  28318  z12bday  28758  axcontlem2  29430  elntg2  29450  redwlklem  30137  redwlk  30138  crctcshwlkn0lem3  30288  crctcshwlkn0lem5  30290  clwwlkext2edg  30534  wwlksubclwwlk  30536  loop1cycl  30631  frgrwopregasn  30804  frgrwopregbsn  30805  blocnilem  31293  ip2eqi  31345  ubthlem2  31360  hial0  31591  hial02  31592  hial2eq  31595  h1datomi  32070  sumspansn  32138  lnopcnbd  32525  riesz4i  32552  bra11  32597  pjss2coi  32653  pjnormssi  32657  pjorthcoi  32658  pjclem4a  32687  pj3lem1  32695  pj3cor1i  32698  hst1h  32716  stm1i  32732  strlem1  32739  golem2  32761  mdbr2  32785  dmdbr5  32797  mdsl2i  32811  atexch  32870  atcvatlem  32874  chirredlem1  32879  cdjreui  32921  cdj1i  32922  cdj3lem1  32923  xraddge02  33236  submarchi  33634  isarchiofld  33647  esumcvg  34604  bnj1468  35363  erdsze2lem2  35791  btwnexch  36613  btwncolinear2  36658  btwncolinear3  36659  btwncolinear4  36660  btwncolinear5  36661  btwncolinear6  36662  nn0prpw  36950  cldbnd  36953  onsuct0  37068  onint1  37076  bj-ceqsalt0  37635  bj-ceqsalt1  37636  bj-inftyexpiinj  37969  bj-bary1lem1  38071  bj-bary1  38072  relowlssretop  38125  isinf2  38167  ltflcei  38370  tan2h  38374  poimirlem26  38403  poimirlem31  38408  ftc1anclem6  38455  dvasin  38461  dvacos  38462  fdc  38503  caushft  38519  heibor1lem  38567  bfplem2  38581  rrncmslem  38590  rngosn3  38682  mpobi123f  38918  riotasv3d  39841  lsatcv1  39929  lub0N  40070  glb0N  40074  oplecon3b  40081  cmtbr4N  40136  cvrnbtwn2  40156  atnlt  40194  atlatle  40201  cvlsupr2  40224  cvrexchlem  40300  cvratlem  40302  atcvrj0  40309  cvrat4  40324  cvrat42  40325  4noncolr3  40334  ps-1  40358  llnnlt  40404  lplnnlt  40446  lvolnltN  40499  dalempnes  40532  dalemqnet  40533  dalem-cly  40552  dalem44  40597  pmaple  40642  cdlemblem  40674  paddss  40726  2polcon4bN  40799  ltrneq2  41029  cdlemc3  41074  cdleme11h  41147  cdleme16b  41160  cdlemednpq  41180  tendospcanN  41904  dihmeetlem13N  42200  mapdordlem2  42518  mapdn0  42550  rspcsbnea  43005  ccatcan2d  43126  ctbnfien  43667  rmxypairf1o  43760  monotoddzzfi  43791  oddcomabszz  43793  acongtr  43827  onsupnmax  44077  onsupsucismax  44128  frege124d  44609  expgrowth  45167  sbcbi  45370  limsupmnflem  46556  funressnfv  47939  funfocofob  47974  2elfz2melfz  48214  iccpartnel  48346  requad2  48547  grlictr  48939  gpg5nbgrvtx13starlem1  48995  gpg5nbgrvtx13starlem3  48997  uzlidlring  49158  ply1mulgsumlem2  49325  fllog2  49506  dignn0flhalflem1  49553