Theorem sylibrd 261

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 250	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
4	1, 3	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  3imtr4d  296  sbciegft  3810  opeldmd  5777  elreldm  5807  ordtr2  6237  ssimaex  6750  fliftfun  7067  isopolem  7100  isosolem  7102  ordsucss  7535  f1oweALT  7675  fnse  7829  brtpos  7903  issmo2  7988  seqomlem1  8088  omcl  8163  oecl  8164  oawordeulem  8182  oaass  8189  omordi  8194  omord  8196  odi  8207  oen0  8214  oeordi  8215  oeordsuc  8222  nnmcl  8240  nnecl  8241  nnmordi  8259  nnmord  8260  nnmwordri  8264  nnaordex  8266  swoord1  8322  ecopovtrn  8402  f1domg  8531  pw2f1olem  8623  domtriord  8665  mapen  8683  mapxpen  8685  mapunen  8688  nndomo  8714  inficl  8891  supmo  8918  infmo  8961  inf3lem6  9098  cantnflem1  9154  tcmin  9185  tcrank  9315  cardne  9396  cardlim  9403  cardsdomel  9405  carduni  9412  alephord  9503  cardinfima  9525  dfac5lem4  9554  infdif2  9634  cofsmo  9693  cfcoflem  9696  infpssrlem4  9730  infpssrlem5  9731  fin4en1  9733  isfin2-2  9743  enfin2i  9745  fin23lem27  9752  isf32lem12  9788  isf34lem6  9804  domtriomlem  9866  cardmin  9988  fpwwe2lem12  10065  inar1  10199  gruiun  10223  ltsonq  10393  prub  10418  reclem3pr  10473  mulcmpblnr  10495  mulgt0sr  10529  axpre-sup  10593  leltadd  11126  infm3  11602  peano5nni  11643  zextle  12058  prime  12066  uzin  12281  ublbneg  12336  zbtwnre  12349  mul2lt0bi  12498  xrre2  12566  xralrple  12601  xmulneg1  12665  supxrbnd  12724  supxrgtmnf  12725  fzrevral  12995  flge  13178  ceile  13220  modadd1  13279  modmul1  13295  modsumfzodifsn  13315  seqcl2  13391  facdiv  13650  hashss  13773  hash2exprb  13832  elfzelfzccat  13936  repswswrd  14148  cshf1  14174  cshwcsh2id  14192  rlim2lt  14856  rlim3  14857  o1lo1  14896  climshftlem  14933  o1co  14945  o1of2  14971  isercolllem2  15024  isercoll  15026  caucvgrlem2  15033  climcndslem2  15207  sqrt2irr  15604  dvds2lem  15624  dvdsle  15662  dvdsfac  15678  ltoddhalfle  15712  divalglem0  15746  ndvdsadd  15763  bitsinv1lem  15792  sadcaddlem  15808  dvdslegcd  15855  bezoutlem2  15890  bezoutlem4  15892  gcdzeq  15904  algcvga  15925  rpdvds  16006  cncongr1  16013  cncongr2  16014  prmind2  16031  isprm6  16060  rpexp  16066  eulerthlem2  16121  pclem  16177  pceulem  16184  pc2dvds  16217  fldivp1  16235  infpnlem1  16248  prmunb  16252  mrieqv2d  16912  plttr  17582  clatl  17728  issubg4  18300  gexdvds  18711  pgpssslw  18741  sylow2alem2  18745  efgs1b  18864  efgsfo  18867  lspindpi  19906  pf1ind  20520  psgnodpm  20734  psgndif  20748  obselocv  20874  mdetunilem9  21231  fiinbas  21562  bastg  21576  tgcl  21579  opnssneib  21725  clslp  21758  tgcnp  21863  iscnp4  21873  cncls2  21883  cncls  21884  cnntr  21885  cnpresti  21898  lmss  21908  lmcnp  21914  cmpsub  22010  tgcmp  22011  dfconn2  22029  t1connperf  22046  1stcfb  22055  1stcrest  22063  kgenss  22153  llycmpkgen2  22160  txdis  22242  qtoptop2  22309  kqt0lem  22346  isr0  22347  regr1lem2  22350  cmphaushmeo  22410  fbun  22450  ssfg  22482  fgtr  22500  ufildr  22541  cnpflf  22611  fclsnei  22629  flimfnfcls  22638  fclscmp  22640  ufilcmp  22642  cnpfcf  22651  alexsublem  22654  alexsubALTlem3  22659  alexsubALTlem4  22660  ptcmplem3  22664  tgphaus  22727  tgpt1  22728  tsmsres  22754  imasdsf1olem  22985  xblss2ps  23013  xblss2  23014  blsscls2  23116  metequiv2  23122  stdbdxmet  23127  nmoi  23339  reconn  23438  mulc1cncf  23515  cncfco  23517  iccpnfhmeo  23551  xrhmeo  23552  evth  23565  pi1grplem  23655  fgcfil  23876  ivthlem2  24055  ivthlem3  24056  ovolicc2lem4  24123  voliunlem1  24153  ioombl1lem4  24164  itg2gt0  24363  limcco  24493  lhop1  24613  tdeglem4  24656  plypf1  24804  coeeulem  24816  coeidlem  24829  coeid3  24832  plymul0or  24872  dvnply2  24878  plydivex  24888  vieta1lem2  24902  plyexmo  24904  aaliou3lem2  24934  ulmss  24987  ulmdvlem3  24992  iblulm  24997  sincosq2sgn  25087  sincosq3sgn  25088  sincosq4sgn  25089  logcnlem5  25231  dcubic  25426  amgm  25570  isnsqf  25714  mumullem2  25759  chtublem  25789  chtub  25790  fsumvma2  25792  vmasum  25794  dchrfi  25833  bposlem1  25862  bposlem3  25864  bposlem7  25868  lgsdir  25910  lgsquadlem2  25959  2sqlem8a  26003  2sqlem10  26006  dchrisum0flb  26088  pntpbnd1  26164  pntlemf  26183  pntlem3  26187  axeuclid  26751  uspgrushgr  26962  uspgrupgr  26963  usgruspgr  26965  usgr2pth  27547  crctcshwlkn0lem5  27594  wwlksnext  27673  wwlksnextsurj  27680  clwwlkccatlem  27769  clwlkclwwlkf  27788  clwwisshclwwslemlem  27793  lnon0  28577  normpyc  28925  ocsh  29062  ocorth  29070  ococss  29072  shsel2  29101  hsupss  29120  pjhth  29172  shlub  29193  cm2j  29399  lnfncnbd  29836  riesz1  29844  rnbra  29886  leopadd  29911  leopmuli  29912  hstles  30010  stge1i  30017  stle0i  30018  dmdbr5  30087  ssmd2  30091  superpos  30133  chcv1  30134  atoml2i  30162  chirredlem2  30170  atcvat3i  30175  mdsymlem5  30186  mdsymlem6  30187  sumdmdii  30194  sumdmdlem2  30198  isarchiofld  30892  sqsscirc2  31154  cnre2csqlem  31155  xrge0iifiso  31180  sigaclci  31393  omssubadd  31560  eulerpartlemb  31628  ballotlemimin  31765  ballotlem7  31795  subgrwlk  32381  cusgracyclt3v  32405  cvmlift2lem12  32563  fmlasucdisj  32648  dfon2lem8  33037  soseq  33098  segconeq  33473  ifscgr  33507  brofs2  33540  brifs2  33541  endofsegid  33548  dissneqlem  34623  rdgellim  34659  fvineqsneq  34695  tan2h  34886  matunitlindflem2  34891  poimirlem31  34925  poimir  34927  fzmul  35018  fdc  35022  incsequz2  35026  sstotbnd2  35054  sstotbnd3  35056  totbndbnd  35069  isexid2  35135  ispridl2  35318  mpobi123f  35442  riotasvd  36094  lsator0sp  36139  lssatle  36153  lshpset2N  36257  lkrlspeqN  36309  omllaw2N  36382  cmtbr3N  36392  lecmtN  36394  cvlcvr1  36477  cvrval4N  36552  cvrat3  36580  3noncolr2  36587  4noncolr3  36591  3dimlem3  36599  3dimlem3OLDN  36600  3dimlem4  36602  3dimlem4OLDN  36603  llncvrlpln  36696  lplncvrlvol  36754  snatpsubN  36888  linepsubN  36890  pmapjat1  36991  pclfinclN  37088  pl42N  37121  ltrneq2  37286  cdleme7aa  37380  cdleme18d  37433  cdleme21b  37464  trlord  37707  trlcoat  37861  dochkrshp  38524  lcfl8  38640  irrapxlem2  39427  pell14qrdich  39473  monotoddzz  39547  pw2f1ocnv  39641  iocinico  39825  nndomog  39904  harval3  39911  sbcim2g  40879  stoweidlem62  42354  elfzelfzlble  43528  eenglngeehlnmlem2  44732