Theorem sylibrd 259

Description: A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

Hypotheses

Ref	Expression
sylibrd.1	⊢ (𝜑 → (𝜓 → 𝜒))
sylibrd.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))

Assertion

Ref	Expression
sylibrd	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem sylibrd

Step	Hyp	Ref	Expression
1		sylibrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		sylibrd.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	2	biimprd 248	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3imtr4d  294  sbciegftOLD  3767  opeldmd  5853  elreldm  5882  predtrss  6278  ordtr2  6360  ssimaex  6917  fliftfun  7258  isopolem  7291  isosolem  7293  ordsucss  7760  f1oweALT  7916  fnse  8074  soseq  8100  brtpos  8176  issmo2  8280  seqomlem1  8380  omcl  8462  oecl  8463  oawordeulem  8480  oaass  8487  omordi  8492  omord  8494  odi  8505  oen0  8513  oeordi  8514  oeordsuc  8521  nnmcl  8539  nnecl  8540  nnmordi  8558  nnmord  8559  nnmwordri  8563  nnaordex  8565  swoord1  8667  ecopovtrn  8758  f1domg  8909  pw2f1olem  9010  domtriord  9052  mapen  9070  mapxpen  9072  mapunen  9075  nndomog  9138  onomeneq  9139  inficl  9329  supmo  9356  infmo  9401  inf3lem6  9543  cantnflem1  9599  tcmin  9649  tcrank  9797  cardne  9878  cardlim  9885  cardsdomel  9887  carduni  9894  alephord  9986  cardinfima  10008  dfac5lem4  10037  dfac5lem4OLD  10039  infdif2  10120  cofsmo  10180  cfcoflem  10183  infpssrlem4  10217  infpssrlem5  10218  fin4en1  10220  isfin2-2  10230  enfin2i  10232  fin23lem27  10239  isf32lem12  10275  isf34lem6  10291  domtriomlem  10353  cardmin  10475  fpwwe2lem11  10553  inar1  10687  gruiun  10711  ltsonq  10881  prub  10906  reclem3pr  10961  mulcmpblnr  10983  mulgt0sr  11017  axpre-sup  11081  leltadd  11623  infm3  12104  peano5nni  12166  zextle  12591  prime  12599  uzin  12813  ublbneg  12872  zbtwnre  12885  mul2lt0bi  13039  xrre2  13111  xralrple  13146  xmulneg1  13210  supxrbnd  13269  supxrgtmnf  13270  fzrevral  13555  flge  13753  ceile  13797  modadd1  13856  modmul1  13875  modsumfzodifsn  13895  seqcl2  13971  facdiv  14238  hashss  14360  hash2exprb  14422  elfzelfzccat  14531  repswswrd  14735  cshf1  14761  cshwcsh2id  14779  rlim2lt  15448  rlim3  15449  o1lo1  15488  climshftlem  15525  o1co  15537  o1of2  15564  isercolllem2  15617  isercoll  15619  caucvgrlem2  15626  climcndslem2  15804  sqrt2irr  16205  dvds2lem  16226  dvdsle  16268  dvdsfac  16284  ltoddhalfle  16319  divalglem0  16351  ndvdsadd  16368  bitsinv1lem  16399  sadcaddlem  16415  dvdslegcd  16462  bezoutlem2  16498  bezoutlem4  16500  gcdzeq  16510  algcvga  16537  rpdvds  16618  cncongr1  16625  cncongr2  16626  prmind2  16643  isprm6  16673  rpexp  16681  eulerthlem2  16741  pclem  16798  pceulem  16805  pc2dvds  16839  fldivp1  16857  infpnlem1  16870  prmunb  16874  mrieqv2d  17594  plttr  18295  clatl  18463  issubg4  19110  gexdvds  19548  pgpssslw  19578  sylow2alem2  19582  efgs1b  19700  efgsfo  19703  imasabl  19840  lspindpi  21120  psgnodpm  21576  psgndif  21590  obselocv  21716  pf1ind  22329  mdetunilem9  22594  fiinbas  22926  bastg  22940  tgcl  22943  opnssneib  23089  clslp  23122  tgcnp  23227  iscnp4  23237  cncls2  23247  cncls  23248  cnntr  23249  cnpresti  23262  lmss  23272  lmcnp  23278  cmpsub  23374  tgcmp  23375  dfconn2  23393  t1connperf  23410  1stcfb  23419  1stcrest  23427  kgenss  23517  llycmpkgen2  23524  txdis  23606  qtoptop2  23673  kqt0lem  23710  isr0  23711  regr1lem2  23714  cmphaushmeo  23774  fbun  23814  ssfg  23846  fgtr  23864  ufildr  23905  cnpflf  23975  fclsnei  23993  flimfnfcls  24002  fclscmp  24004  ufilcmp  24006  cnpfcf  24015  alexsublem  24018  alexsubALTlem3  24023  alexsubALTlem4  24024  ptcmplem3  24028  tgphaus  24091  tgpt1  24092  tsmsres  24118  imasdsf1olem  24347  xblss2ps  24375  xblss2  24376  blsscls2  24478  metequiv2  24484  stdbdxmet  24489  nmoi  24702  reconn  24803  mulc1cncf  24881  cncfco  24883  iccpnfhmeo  24921  xrhmeo  24922  evth  24935  pi1grplem  25025  fgcfil  25247  ivthlem2  25428  ivthlem3  25429  ovolicc2lem4  25496  voliunlem1  25526  ioombl1lem4  25537  itg2gt0  25736  limcco  25869  lhop1  25991  tdeglem4  26037  plypf1  26189  coeeulem  26201  coeidlem  26214  coeid3  26217  plymul0or  26259  dvnply2  26266  plydivex  26276  vieta1lem2  26290  plyexmo  26292  aaliou3lem2  26322  ulmss  26377  ulmdvlem3  26382  iblulm  26387  sincosq2sgn  26479  sincosq3sgn  26480  sincosq4sgn  26481  logcnlem5  26626  dcubic  26827  amgm  26972  isnsqf  27116  mumullem2  27161  chtublem  27193  chtub  27194  fsumvma2  27196  vmasum  27198  dchrfi  27237  bposlem1  27266  bposlem3  27268  bposlem7  27272  lgsdir  27314  lgsquadlem2  27363  2sqlem8a  27407  2sqlem10  27410  dchrisum0flb  27492  pntpbnd1  27568  pntlemf  27587  pntlem3  27591  addonbday  28290  peano5uzs  28415  axeuclid  29051  uspgrushgr  29265  uspgrupgr  29266  usgruspgr  29268  usgr2pth  29852  crctcshwlkn0lem5  29902  wwlksnext  29981  wwlksnextsurj  29988  clwwlkccatlem  30079  clwlkclwwlkf  30098  clwwisshclwwslemlem  30103  lnon0  30889  normpyc  31237  ocsh  31374  ocorth  31382  ococss  31384  shsel2  31413  hsupss  31432  pjhth  31484  shlub  31505  cm2j  31711  lnfncnbd  32148  riesz1  32156  rnbra  32198  leopadd  32223  leopmuli  32224  hstles  32322  stge1i  32329  stle0i  32330  dmdbr5  32399  ssmd2  32403  superpos  32445  chcv1  32446  atoml2i  32474  chirredlem2  32482  atcvat3i  32487  mdsymlem5  32498  mdsymlem6  32499  sumdmdii  32506  sumdmdlem2  32510  isarchiofld  33280  sqsscirc2  34074  cnre2csqlem  34075  xrge0iifiso  34100  sigaclci  34297  omssubadd  34465  eulerpartlemb  34533  ballotlemimin  34671  ballotlem7  34701  fineqvac  35281  fineqvinfep  35290  vonf1owev  35311  subgrwlk  35335  cusgracyclt3v  35359  cvmlift2lem12  35517  fmlasucdisj  35602  dfon2lem8  35991  segconeq  36213  ifscgr  36247  brofs2  36280  brifs2  36281  endofsegid  36288  dissneqlem  37667  rdgellim  37703  fvineqsneq  37739  tan2h  37944  matunitlindflem2  37949  poimirlem31  37983  poimir  37985  fzmul  38073  fdc  38077  incsequz2  38081  sstotbnd2  38106  sstotbnd3  38108  totbndbnd  38121  isexid2  38187  ispridl2  38370  mpobi123f  38494  disjlem18  39235  disjdmqsss  39237  eldisjs6  39272  riotasvd  39413  lsator0sp  39458  lssatle  39472  lshpset2N  39576  lkrlspeqN  39628  omllaw2N  39701  cmtbr3N  39711  lecmtN  39713  cvlcvr1  39796  cvrval4N  39871  cvrat3  39899  3noncolr2  39906  4noncolr3  39910  3dimlem3  39918  3dimlem3OLDN  39919  3dimlem4  39921  3dimlem4OLDN  39922  llncvrlpln  40015  lplncvrlvol  40073  snatpsubN  40207  linepsubN  40209  pmapjat1  40310  pclfinclN  40407  pl42N  40440  ltrneq2  40605  cdleme7aa  40699  cdleme18d  40752  cdleme21b  40783  trlord  41026  trlcoat  41180  dochkrshp  41843  lcfl8  41959  mulgt0con1dlem  42925  irrapxlem2  43266  pell14qrdich  43312  monotoddzz  43386  pw2f1ocnv  43480  iocinico  43655  ordnexbtwnsuc  43710  tfsconcat0i  43788  naddwordnexlem4  43844  harval3  43980  sbcim2g  44980  stoweidlem62  46505  elfzelfzlble  47766  pgnbgreunbgrlem1  48586  pgnbgreunbgrlem4  48592  1arymaptf1  49115  2arymaptf1  49126  eenglngeehlnmlem2  49211  mpbiran3d  49269  opnneil  49382