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  3880  rspcsbela  4399  sneqrg  4797  preq1b  4804  csbexg  5267  elrnrexdm  7113  isoselem  7372  funeldmb  7392  riotass2  7430  ordzsl  7880  resf1extb  7970  oaword2  8589  oaordex  8594  omword1  8609  om00  8611  omeulem2  8619  oen0  8623  oeeui  8639  nnaordex  8675  php3  9252  frfi  9304  infglb  9510  suc11reg  9647  cardne  10073  cardsdomel  10082  carduni  10089  acndom  10157  alephinit  10201  cfflb  10364  cfslb2n  10373  fin23lem28  10445  isf34lem6  10485  fin1a2lem9  10513  axcc3  10543  winalim2  10808  inar1  10887  rankcf  10889  addclprlem2  11129  mulclprlem  11131  ltexprlem7  11154  prlem936  11159  reclem4pr  11162  sqgt0sr  11218  ltord2  11872  leord2  11873  eqord2  11874  mulge0b  12214  lt2halves  12608  addltmul  12609  ltsubnn0  12684  nzadd  12771  zextlt  12800  recnz  12801  zeo  12812  peano5uzi  12815  uzm1  13026  irradd  13128  irrmul  13129  xltneg  13374  xleadd1  13412  xmulasslem  13442  xlemul1a  13445  xlemul1  13447  fznuz  13770  uznfz  13771  axdc4uzlem  14153  facndiv  14459  hashvnfin  14531  hashgt12el  14594  hashgt12el2  14595  hashf1  14629  ccatalpha  14767  swrdccatin2  14906  swrdccatin2d  14921  rennim  15435  cau3lem  15551  caubnd2  15554  o1lo1  15733  climrlim2  15743  climshft  15772  subcn2  15791  mulcn2  15792  rlimo1  15813  o1dif  15826  isercoll  15864  caucvgrlem  15869  serf0  15877  cvgrat  16081  efieq1re  16396  moddvds  16462  dvdsssfz1  16517  smuval2  16681  nn0seqcvgd  16774  algcvgblem  16781  eucalglt  16789  lcmgcdlem  16810  rpmul  16863  divgcdcoprm0  16869  isprm6  16919  rpexp  16927  eulerthlem2  16988  prmdiv  16991  pcprendvds2  17048  pcz  17088  pcprmpw  17090  pcadd2  17097  pcfac  17106  expnprm  17109  ramlb  17226  firest  17632  joineu  18583  meeteu  18597  latjlej1  18656  latjlej2  18657  latmlem1  18672  latmlem2  18673  lubun  18718  acsmapd  18757  idressid  18891  imasgrp2  19294  issubg4  19385  psgnunilem4  19741  oddvdsnn0  19788  odmulgeq  19801  subgpgp  19841  odcau  19848  lsmlub  19908  frgpnabllem1  20117  pgpfac1lem2  20321  pgpfac1lem3a  20322  pgpfac1lem3  20323  irredrmul  20687  isdomn4  20997  islmhm2  21343  lsmelval2  21390  lspsnat  21453  znidomb  21897  ip2eq  21989  lsmcss  22028  cnpnei  23612  cncls2  23621  cncls  23622  cnntr  23623  cnt0  23694  isnrm2  23706  comppfsc  23881  kqcldsat  24082  isr0  24086  hmeoopn  24115  hmeocld  24116  trufil  24259  opnsubg  24457  ghmcnp  24464  tgphaus  24466  qustgpopn  24469  tsmsgsum  24488  isngp4  24961  xrhmeo  25297  bndth  25309  cfilres  25647  caubl  25659  ivthlem2  25803  ovolicc2  25873  ismbf3d  26005  itg1ge0a  26062  mbfi1flim  26074  itg2gt0  26111  dvge0  26356  dvcnvrelem1  26367  dvcvx  26370  mdegmullem  26426  ig1peu  26523  plyco  26590  coemulc  26604  dgreq0  26614  dgrlt  26615  plymul0or  26629  plydiveu  26649  quotcan  26662  aalioulem3  26691  ulmcaulem  26751  sincosq3sgn  26859  sincosq4sgn  26860  sineq0  26882  logrec  27121  xrlimcnp  27326  cxploglim  27335  lgamgulmlem1  27386  mumul  27538  chtub  27569  perfect1  27585  dchrelbas3  27595  lgsdir2lem4  27685  lgsne0  27692  lgsquad2lem2  27742  2sqlem8a  27782  2sqblem  27788  nogt01o  28083  ltslpss  28324  ltadds2im  28402  ltnegs  28461  z12bday  28901  axcontlem2  29573  elntg2  29593  redwlklem  30280  redwlk  30281  crctcshwlkn0lem3  30431  crctcshwlkn0lem5  30433  clwwlkext2edg  30677  wwlksubclwwlk  30679  loop1cycl  30774  frgrwopregasn  30947  frgrwopregbsn  30948  blocnilem  31436  ip2eqi  31488  ubthlem2  31503  hial0  31734  hial02  31735  hial2eq  31738  h1datomi  32213  sumspansn  32281  lnopcnbd  32668  riesz4i  32695  bra11  32740  pjss2coi  32796  pjnormssi  32800  pjorthcoi  32801  pjclem4a  32830  pj3lem1  32838  pj3cor1i  32841  hst1h  32859  stm1i  32875  strlem1  32882  golem2  32904  mdbr2  32928  dmdbr5  32940  mdsl2i  32954  atexch  33013  atcvatlem  33017  chirredlem1  33022  cdjreui  33064  cdj1i  33065  cdj3lem1  33066  xraddge02  33419  submarchi  33817  isarchiofld  33830  esumcvg  34788  bnj1468  35546  j00smo  36005  j0ltaleph  36008  erdsze2lem2  36136  btwnexch  36968  btwncolinear2  37013  btwncolinear3  37014  btwncolinear4  37015  btwncolinear5  37016  btwncolinear6  37017  nn0prpw  37289  cldbnd  37292  onsuct0  37407  onint1  37415  bj-ceqsalt0  37974  bj-ceqsalt1  37975  bj-inftyexpiinj  38322  bj-bary1lem1  38424  bj-bary1  38425  relowlssretop  38478  isinf2  38520  ltflcei  38723  tan2h  38727  poimirlem26  38756  poimirlem31  38761  ftc1anclem6  38808  dvasin  38814  dvacos  38815  fdc  38871  caushft  38887  heibor1lem  38935  bfplem2  38949  rrncmslem  38958  rngosn3  39050  mpobi123f  39286  riotasv3d  40209  lsatcv1  40297  lub0N  40438  glb0N  40442  oplecon3b  40449  cmtbr4N  40504  cvrnbtwn2  40524  atnlt  40562  atlatle  40569  cvlsupr2  40592  cvrexchlem  40668  cvratlem  40670  atcvrj0  40677  cvrat4  40692  cvrat42  40693  4noncolr3  40702  ps-1  40726  llnnlt  40772  lplnnlt  40814  lvolnltN  40867  dalempnes  40900  dalemqnet  40901  dalem-cly  40920  dalem44  40965  pmaple  41010  cdlemblem  41042  paddss  41094  2polcon4bN  41167  ltrneq2  41397  cdlemc3  41442  cdleme11h  41515  cdleme16b  41528  cdlemednpq  41548  tendospcanN  42272  dihmeetlem13N  42568  mapdordlem2  42886  mapdn0  42918  rspcsbnea  43373  ccatcan2d  43495  ctbnfien  44018  rmxypairf1o  44111  monotoddzzfi  44142  oddcomabszz  44144  acongtr  44178  onsupnmax  44422  onsupsucismax  44473  frege124d  44953  expgrowth  45511  sbcbi  45713  hfstructwe  46234  limsupmnflem  46935  funressnfv  48318  funfocofob  48353  2elfz2melfz  48593  iccpartnel  48725  requad2  48926  grlictr  49318  gpg5nbgrvtx13starlem1  49374  gpg5nbgrvtx13starlem3  49376  uzlidlring  49537  ply1mulgsumlem2  49704  fllog2  49885  dignn0flhalflem1  49932