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  3875  rspcsbela  4395  sneqrg  4793  preq1b  4800  csbexg  5263  elrnrexdm  7089  isoselem  7349  funeldmb  7369  riotass2  7407  ordzsl  7856  resf1extb  7946  oaword2  8564  oaordex  8569  omword1  8584  om00  8586  omeulem2  8594  oen0  8598  oeeui  8614  nnaordex  8650  php3  9227  frfi  9279  infglb  9486  suc11reg  9623  cardne  10049  cardsdomel  10058  carduni  10065  acndom  10133  alephinit  10177  cfflb  10340  cfslb2n  10349  fin23lem28  10421  isf34lem6  10461  fin1a2lem9  10489  axcc3  10519  winalim2  10784  inar1  10863  rankcf  10865  addclprlem2  11105  mulclprlem  11107  ltexprlem7  11130  prlem936  11135  reclem4pr  11138  sqgt0sr  11194  ltord2  11848  leord2  11849  eqord2  11850  mulge0b  12190  lt2halves  12584  addltmul  12585  ltsubnn0  12660  nzadd  12747  zextlt  12776  recnz  12777  zeo  12788  peano5uzi  12791  uzm1  13002  irradd  13104  irrmul  13105  xltneg  13350  xleadd1  13388  xmulasslem  13418  xlemul1a  13421  xlemul1  13423  fznuz  13746  uznfz  13747  axdc4uzlem  14129  facndiv  14435  hashvnfin  14507  hashgt12el  14570  hashgt12el2  14571  hashf1  14605  ccatalpha  14743  swrdccatin2  14882  swrdccatin2d  14897  rennim  15411  cau3lem  15527  caubnd2  15530  o1lo1  15709  climrlim2  15719  climshft  15748  subcn2  15767  mulcn2  15768  rlimo1  15789  o1dif  15802  isercoll  15840  caucvgrlem  15845  serf0  15853  cvgrat  16057  efieq1re  16372  moddvds  16438  dvdsssfz1  16493  smuval2  16657  nn0seqcvgd  16750  algcvgblem  16757  eucalglt  16765  lcmgcdlem  16786  rpmul  16839  divgcdcoprm0  16845  isprm6  16895  rpexp  16903  eulerthlem2  16964  prmdiv  16967  pcprendvds2  17024  pcz  17064  pcprmpw  17066  pcadd2  17073  pcfac  17082  expnprm  17085  ramlb  17202  firest  17608  joineu  18559  meeteu  18573  latjlej1  18632  latjlej2  18633  latmlem1  18648  latmlem2  18649  lubun  18694  acsmapd  18733  idressid  18867  imasgrp2  19270  issubg4  19361  psgnunilem4  19716  oddvdsnn0  19763  odmulgeq  19776  subgpgp  19816  odcau  19823  lsmlub  19883  frgpnabllem1  20092  pgpfac1lem2  20296  pgpfac1lem3a  20297  pgpfac1lem3  20298  irredrmul  20662  isdomn4  20972  islmhm2  21318  lsmelval2  21365  lspsnat  21428  znidomb  21872  ip2eq  21964  lsmcss  22003  cnpnei  23587  cncls2  23596  cncls  23597  cnntr  23598  cnt0  23669  isnrm2  23681  comppfsc  23856  kqcldsat  24057  isr0  24061  hmeoopn  24090  hmeocld  24091  trufil  24234  opnsubg  24432  ghmcnp  24439  tgphaus  24441  qustgpopn  24444  tsmsgsum  24463  isngp4  24936  xrhmeo  25272  bndth  25284  cfilres  25622  caubl  25634  ivthlem2  25778  ovolicc2  25848  ismbf3d  25980  itg1ge0a  26037  mbfi1flim  26049  itg2gt0  26086  dvge0  26331  dvcnvrelem1  26342  dvcvx  26345  mdegmullem  26401  ig1peu  26498  plyco  26565  coemulc  26579  dgreq0  26589  dgrlt  26590  plymul0or  26604  plydiveu  26624  quotcan  26637  aalioulem3  26666  ulmcaulem  26726  sincosq3sgn  26834  sincosq4sgn  26835  sineq0  26857  logrec  27096  xrlimcnp  27301  cxploglim  27310  lgamgulmlem1  27361  mumul  27513  chtub  27544  perfect1  27560  dchrelbas3  27570  lgsdir2lem4  27660  lgsne0  27667  lgsquad2lem2  27717  2sqlem8a  27757  2sqblem  27763  nogt01o  28058  ltslpss  28299  ltadds2im  28377  ltnegs  28436  z12bday  28876  axcontlem2  29548  elntg2  29568  redwlklem  30255  redwlk  30256  crctcshwlkn0lem3  30406  crctcshwlkn0lem5  30408  clwwlkext2edg  30652  wwlksubclwwlk  30654  loop1cycl  30749  frgrwopregasn  30922  frgrwopregbsn  30923  blocnilem  31411  ip2eqi  31463  ubthlem2  31478  hial0  31709  hial02  31710  hial2eq  31713  h1datomi  32188  sumspansn  32256  lnopcnbd  32643  riesz4i  32670  bra11  32715  pjss2coi  32771  pjnormssi  32775  pjorthcoi  32776  pjclem4a  32805  pj3lem1  32813  pj3cor1i  32816  hst1h  32834  stm1i  32850  strlem1  32857  golem2  32879  mdbr2  32903  dmdbr5  32915  mdsl2i  32929  atexch  32988  atcvatlem  32992  chirredlem1  32997  cdjreui  33039  cdj1i  33040  cdj3lem1  33041  xraddge02  33395  submarchi  33793  isarchiofld  33806  esumcvg  34764  bnj1468  35522  j00smo  35944  j0ltaleph  35947  erdsze2lem2  36055  btwnexch  36882  btwncolinear2  36927  btwncolinear3  36928  btwncolinear4  36929  btwncolinear5  36930  btwncolinear6  36931  nn0prpw  37203  cldbnd  37206  onsuct0  37321  onint1  37329  bj-ceqsalt0  37888  bj-ceqsalt1  37889  bj-inftyexpiinj  38223  bj-bary1lem1  38325  bj-bary1  38326  relowlssretop  38379  isinf2  38421  ltflcei  38624  tan2h  38628  poimirlem26  38657  poimirlem31  38662  ftc1anclem6  38709  dvasin  38715  dvacos  38716  fdc  38772  caushft  38788  heibor1lem  38836  bfplem2  38850  rrncmslem  38859  rngosn3  38951  mpobi123f  39187  riotasv3d  40110  lsatcv1  40198  lub0N  40339  glb0N  40343  oplecon3b  40350  cmtbr4N  40405  cvrnbtwn2  40425  atnlt  40463  atlatle  40470  cvlsupr2  40493  cvrexchlem  40569  cvratlem  40571  atcvrj0  40578  cvrat4  40593  cvrat42  40594  4noncolr3  40603  ps-1  40627  llnnlt  40673  lplnnlt  40715  lvolnltN  40768  dalempnes  40801  dalemqnet  40802  dalem-cly  40821  dalem44  40866  pmaple  40911  cdlemblem  40943  paddss  40995  2polcon4bN  41068  ltrneq2  41298  cdlemc3  41343  cdleme11h  41416  cdleme16b  41429  cdlemednpq  41449  tendospcanN  42173  dihmeetlem13N  42469  mapdordlem2  42787  mapdn0  42819  rspcsbnea  43274  ccatcan2d  43395  ctbnfien  43918  rmxypairf1o  44011  monotoddzzfi  44042  oddcomabszz  44044  acongtr  44078  onsupnmax  44323  onsupsucismax  44374  frege124d  44854  expgrowth  45412  sbcbi  45615  limsupmnflem  46823  funressnfv  48206  funfocofob  48241  2elfz2melfz  48481  iccpartnel  48613  requad2  48814  grlictr  49206  gpg5nbgrvtx13starlem1  49262  gpg5nbgrvtx13starlem3  49264  uzlidlring  49425  ply1mulgsumlem2  49592  fllog2  49773  dignn0flhalflem1  49820