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  ceqsalt  3463  sbceqalOLD  3784  csbiebt  3863  rspcsbela  4370  sneqrg  4771  preq1b  4778  csbexg  5235  elrnrexdm  6974  isoselem  7221  riotass2  7272  ordzsl  7701  oaword2  8393  oaordex  8398  omword1  8413  om00  8415  omeulem2  8423  oen0  8426  oeeui  8442  nnaordex  8478  php3  9004  php3OLD  9016  onomeneqOLD  9021  frfi  9068  infglb  9258  suc11reg  9386  cardne  9732  cardsdomel  9741  carduni  9748  acndom  9816  alephinit  9860  cfflb  10024  cfslb2n  10033  fin23lem28  10105  isf34lem6  10145  fin1a2lem9  10173  axcc3  10203  winalim2  10461  inar1  10540  rankcf  10542  addclprlem2  10782  mulclprlem  10784  ltexprlem7  10807  prlem936  10812  reclem4pr  10815  sqgt0sr  10871  ltord2  11513  leord2  11514  eqord2  11515  mulgt1  11843  mulge0b  11854  lt2halves  12217  addltmul  12218  ltsubnn0  12293  nzadd  12377  zextlt  12403  recnz  12404  zeo  12415  peano5uzi  12418  uzm1  12625  irradd  12722  irrmul  12723  xltneg  12960  xleadd1  12998  xmulasslem  13028  xlemul1a  13031  xlemul1  13033  fznuz  13347  uznfz  13348  axdc4uzlem  13712  facndiv  14011  hashvnfin  14084  hashgt12el  14146  hashgt12el2  14147  hashf1  14180  ccatalpha  14307  swrdccatin2  14451  swrdccatin2d  14466  rennim  14959  cau3lem  15075  caubnd2  15078  o1lo1  15255  climrlim2  15265  climshft  15294  subcn2  15313  mulcn2  15314  rlimo1  15335  o1dif  15348  isercoll  15388  caucvgrlem  15393  serf0  15401  cvgrat  15604  efieq1re  15917  moddvds  15983  dvdsssfz1  16036  smuval2  16198  nn0seqcvgd  16284  algcvgblem  16291  eucalglt  16299  lcmgcdlem  16320  rpmul  16373  divgcdcoprm0  16379  isprm6  16428  rpexp  16436  eulerthlem2  16492  prmdiv  16495  pcprendvds2  16551  pcz  16591  pcprmpw  16593  pcadd2  16600  pcfac  16609  expnprm  16612  ramlb  16729  firest  17152  joineu  18109  meeteu  18123  latjlej1  18180  latjlej2  18181  latmlem1  18196  latmlem2  18197  lubun  18242  acsmapd  18281  imasgrp2  18699  issubg4  18783  psgnunilem4  19114  oddvdsnn0  19161  odmulgeq  19173  subgpgp  19211  odcau  19218  lsmlub  19279  frgpnabllem1  19483  pgpfac1lem2  19687  pgpfac1lem3a  19688  pgpfac1lem3  19689  irredrmul  19958  islmhm2  20309  lsmelval2  20356  lspsnat  20416  znidomb  20778  ip2eq  20867  lsmcss  20906  cnpnei  22424  cncls2  22433  cncls  22434  cnntr  22435  cnt0  22506  isnrm2  22518  comppfsc  22692  kqcldsat  22893  isr0  22897  hmeoopn  22926  hmeocld  22927  trufil  23070  opnsubg  23268  ghmcnp  23275  tgphaus  23277  qustgpopn  23280  tsmsgsum  23299  isngp4  23777  xrhmeo  24118  bndth  24130  cfilres  24469  caubl  24481  ivthlem2  24625  ovolicc2  24695  ismbf3d  24827  itg1ge0a  24885  mbfi1flim  24897  itg2gt0  24934  dvge0  25179  dvcnvrelem1  25190  dvcvx  25193  mdegmullem  25252  ig1peu  25345  plyco  25411  coemulc  25425  dgreq0  25435  dgrlt  25436  plymul0or  25450  plydiveu  25467  quotcan  25478  aalioulem3  25503  ulmcaulem  25562  sincosq3sgn  25666  sincosq4sgn  25667  sineq0  25689  logrec  25922  xrlimcnp  26127  cxploglim  26136  lgamgulmlem1  26187  mumul  26339  chtub  26369  perfect1  26385  dchrelbas3  26395  lgsdir2lem4  26485  lgsne0  26492  lgsquad2lem2  26542  2sqlem8a  26582  2sqblem  26588  axcontlem2  27342  elntg2  27362  redwlklem  28048  redwlk  28049  crctcshwlkn0lem3  28186  crctcshwlkn0lem5  28188  clwwlkext2edg  28429  wwlksubclwwlk  28431  frgrwopregasn  28689  frgrwopregbsn  28690  blocnilem  29175  ip2eqi  29227  ubthlem2  29242  hial0  29473  hial02  29474  hial2eq  29477  h1datomi  29952  sumspansn  30020  lnopcnbd  30407  riesz4i  30434  bra11  30479  pjss2coi  30535  pjnormssi  30539  pjorthcoi  30540  pjclem4a  30569  pj3lem1  30577  pj3cor1i  30580  hst1h  30598  stm1i  30614  strlem1  30621  golem2  30643  mdbr2  30667  dmdbr5  30679  mdsl2i  30693  atexch  30752  atcvatlem  30756  chirredlem1  30761  cdjreui  30803  cdj1i  30804  cdj3lem1  30805  xraddge02  31088  submarchi  31449  isarchiofld  31525  esumcvg  32063  bnj1468  32835  loop1cycl  33108  erdsze2lem2  33175  funeldmb  33746  nogt01o  33908  sltlpss  34096  btwnexch  34336  btwncolinear2  34381  btwncolinear3  34382  btwncolinear4  34383  btwncolinear5  34384  btwncolinear6  34385  nn0prpw  34521  cldbnd  34524  onsuct0  34639  onint1  34647  bj-ceqsalt0  35078  bj-ceqsalt1  35079  bj-inftyexpiinj  35389  bj-bary1lem1  35491  bj-bary1  35492  relowlssretop  35543  isinf2  35585  ltflcei  35774  tan2h  35778  poimirlem26  35812  poimirlem31  35817  ftc1anclem6  35864  dvasin  35870  dvacos  35871  fdc  35912  caushft  35928  heibor1lem  35976  bfplem2  35990  rrncmslem  35999  rngosn3  36091  mpobi123f  36329  riotasv3d  36981  lsatcv1  37069  lub0N  37210  glb0N  37214  oplecon3b  37221  cmtbr4N  37276  cvrnbtwn2  37296  atnlt  37334  atlatle  37341  cvlsupr2  37364  cvrexchlem  37440  cvratlem  37442  atcvrj0  37449  cvrat4  37464  cvrat42  37465  4noncolr3  37474  ps-1  37498  llnnlt  37544  lplnnlt  37586  lvolnltN  37639  dalempnes  37672  dalemqnet  37673  dalem-cly  37692  dalem44  37737  pmaple  37782  cdlemblem  37814  paddss  37866  2polcon4bN  37939  ltrneq2  38169  cdlemc3  38214  cdleme11h  38287  cdleme16b  38300  cdlemednpq  38320  tendospcanN  39044  dihmeetlem13N  39340  mapdordlem2  39658  mapdn0  39690  isdomn4  40179  ccatcan2d  40226  ctbnfien  40647  rmxypairf1o  40740  monotoddzzfi  40771  oddcomabszz  40773  acongtr  40807  frege124d  41376  expgrowth  41960  sbcbi  42166  limsupmnflem  43268  funressnfv  44548  funfocofob  44581  2elfz2melfz  44821  iccpartnel  44901  requad2  45086  uzlidlring  45498  ply1mulgsumlem2  45739  fllog2  45925  dignn0flhalflem1  45972