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  3885  rspcsbela  4406  sneqrg  4809  preq1b  4816  csbexg  5278  elrnrexdm  7091  isoselem  7350  funeldmb  7370  riotass2  7410  ordzsl  7850  resf1extb  7940  oaword2  8547  oaordex  8552  omword1  8567  om00  8569  omeulem2  8577  oen0  8581  oeeui  8597  nnaordex  8633  php3  9203  frfi  9255  infglb  9461  suc11reg  9598  cardne  9970  cardsdomel  9979  carduni  9986  acndom  10054  alephinit  10098  cfflb  10261  cfslb2n  10270  fin23lem28  10342  isf34lem6  10382  fin1a2lem9  10410  axcc3  10440  winalim2  10699  inar1  10778  rankcf  10780  addclprlem2  11020  mulclprlem  11022  ltexprlem7  11045  prlem936  11050  reclem4pr  11053  sqgt0sr  11109  ltord2  11761  leord2  11762  eqord2  11763  mulge0b  12103  lt2halves  12497  addltmul  12498  ltsubnn0  12573  nzadd  12660  zextlt  12688  recnz  12689  zeo  12700  peano5uzi  12703  uzm1  12914  irradd  13015  irrmul  13016  xltneg  13261  xleadd1  13299  xmulasslem  13329  xlemul1a  13332  xlemul1  13334  fznuz  13656  uznfz  13657  axdc4uzlem  14039  facndiv  14344  hashvnfin  14416  hashgt12el  14479  hashgt12el2  14480  hashf1  14514  ccatalpha  14652  swrdccatin2  14790  swrdccatin2d  14805  rennim  15316  cau3lem  15432  caubnd2  15435  o1lo1  15614  climrlim2  15624  climshft  15653  subcn2  15672  mulcn2  15673  rlimo1  15694  o1dif  15707  isercoll  15745  caucvgrlem  15750  serf0  15758  cvgrat  15963  efieq1re  16280  moddvds  16346  dvdsssfz1  16401  smuval2  16565  nn0seqcvgd  16653  algcvgblem  16660  eucalglt  16668  lcmgcdlem  16689  rpmul  16742  divgcdcoprm0  16748  isprm6  16798  rpexp  16806  eulerthlem2  16866  prmdiv  16869  pcprendvds2  16926  pcz  16966  pcprmpw  16968  pcadd2  16975  pcfac  16984  expnprm  16987  ramlb  17104  firest  17510  joineu  18461  meeteu  18475  latjlej1  18534  latjlej2  18535  latmlem1  18550  latmlem2  18551  lubun  18596  acsmapd  18635  idressid  18762  imasgrp2  19152  issubg4  19243  psgnunilem4  19598  oddvdsnn0  19645  odmulgeq  19658  subgpgp  19698  odcau  19705  lsmlub  19765  frgpnabllem1  19974  pgpfac1lem2  20178  pgpfac1lem3a  20179  pgpfac1lem3  20180  irredrmul  20542  isdomn4  20851  islmhm2  21196  lsmelval2  21243  lspsnat  21306  znidomb  21748  ip2eq  21840  lsmcss  21879  cnpnei  23458  cncls2  23467  cncls  23468  cnntr  23469  cnt0  23540  isnrm2  23552  comppfsc  23726  kqcldsat  23927  isr0  23931  hmeoopn  23960  hmeocld  23961  trufil  24104  opnsubg  24302  ghmcnp  24309  tgphaus  24311  qustgpopn  24314  tsmsgsum  24333  isngp4  24806  xrhmeo  25142  bndth  25154  cfilres  25492  caubl  25504  ivthlem2  25648  ovolicc2  25718  ismbf3d  25850  itg1ge0a  25907  mbfi1flim  25919  itg2gt0  25956  dvge0  26202  dvcnvrelem1  26213  dvcvx  26216  mdegmullem  26272  ig1peu  26369  plyco  26435  coemulc  26449  dgreq0  26459  dgrlt  26460  plymul0or  26476  plydiveu  26496  quotcan  26507  aalioulem3  26534  ulmcaulem  26594  sincosq3sgn  26702  sincosq4sgn  26703  sineq0  26726  logrec  26965  xrlimcnp  27170  cxploglim  27179  lgamgulmlem1  27230  mumul  27382  chtub  27413  perfect1  27429  dchrelbas3  27439  lgsdir2lem4  27529  lgsne0  27536  lgsquad2lem2  27586  2sqlem8a  27626  2sqblem  27632  nogt01o  27897  ltslpss  28138  ltadds2im  28216  ltnegs  28275  z12bday  28715  axcontlem2  29352  elntg2  29372  redwlklem  30056  redwlk  30057  crctcshwlkn0lem3  30198  crctcshwlkn0lem5  30200  clwwlkext2edg  30444  wwlksubclwwlk  30446  frgrwopregasn  30704  frgrwopregbsn  30705  blocnilem  31193  ip2eqi  31245  ubthlem2  31260  hial0  31491  hial02  31492  hial2eq  31495  h1datomi  31970  sumspansn  32038  lnopcnbd  32425  riesz4i  32452  bra11  32497  pjss2coi  32553  pjnormssi  32557  pjorthcoi  32558  pjclem4a  32587  pj3lem1  32595  pj3cor1i  32598  hst1h  32616  stm1i  32632  strlem1  32639  golem2  32661  mdbr2  32685  dmdbr5  32697  mdsl2i  32711  atexch  32770  atcvatlem  32774  chirredlem1  32779  cdjreui  32821  cdj1i  32822  cdj3lem1  32823  xraddge02  33139  submarchi  33537  isarchiofld  33550  esumcvg  34507  bnj1468  35266  loop1cycl  35650  erdsze2lem2  35717  btwnexch  36538  btwncolinear2  36583  btwncolinear3  36584  btwncolinear4  36585  btwncolinear5  36586  btwncolinear6  36587  nn0prpw  36875  cldbnd  36878  onsuct0  36993  onint1  37001  bj-ceqsalt0  37560  bj-ceqsalt1  37561  bj-inftyexpiinj  37894  bj-bary1lem1  37996  bj-bary1  37997  relowlssretop  38050  isinf2  38092  ltflcei  38300  tan2h  38304  poimirlem26  38338  poimirlem31  38343  ftc1anclem6  38390  dvasin  38396  dvacos  38397  fdc  38437  caushft  38453  heibor1lem  38501  bfplem2  38515  rrncmslem  38524  rngosn3  38616  mpobi123f  38852  riotasv3d  39775  lsatcv1  39863  lub0N  40004  glb0N  40008  oplecon3b  40015  cmtbr4N  40070  cvrnbtwn2  40090  atnlt  40128  atlatle  40135  cvlsupr2  40158  cvrexchlem  40234  cvratlem  40236  atcvrj0  40243  cvrat4  40258  cvrat42  40259  4noncolr3  40268  ps-1  40292  llnnlt  40338  lplnnlt  40380  lvolnltN  40433  dalempnes  40466  dalemqnet  40467  dalem-cly  40486  dalem44  40531  pmaple  40576  cdlemblem  40608  paddss  40660  2polcon4bN  40733  ltrneq2  40963  cdlemc3  41008  cdleme11h  41081  cdleme16b  41094  cdlemednpq  41114  tendospcanN  41838  dihmeetlem13N  42134  mapdordlem2  42452  mapdn0  42484  rspcsbnea  42939  ccatcan2d  43060  ctbnfien  43586  rmxypairf1o  43679  monotoddzzfi  43710  oddcomabszz  43712  acongtr  43746  onsupnmax  43996  onsupsucismax  44047  frege124d  44528  expgrowth  45086  sbcbi  45289  limsupmnflem  46475  funressnfv  47821  funfocofob  47856  2elfz2melfz  48096  iccpartnel  48228  requad2  48429  grlictr  48821  gpg5nbgrvtx13starlem1  48877  gpg5nbgrvtx13starlem3  48879  uzlidlring  49041  ply1mulgsumlem2  49208  fllog2  49389  dignn0flhalflem1  49436