Theorem sylibrd 260

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  3imtr4d  295  opeldmd  5855  elreldm  5884  predtrss  6280  ordtr2  6362  ssimaex  6919  fliftfun  7263  isopolem  7296  isosolem  7298  ordsucss  7765  f1oweALT  7921  fnse  8080  soseq  8106  brtpos  8182  issmo2  8286  seqomlem1  8386  omcl  8468  oecl  8469  oawordeulem  8486  oaass  8493  omordi  8498  omord  8500  odi  8511  oen0  8519  oeordi  8520  oeordsuc  8527  nnmcl  8545  nnecl  8546  nnmordi  8564  nnmord  8565  nnmwordri  8569  nnaordex  8571  swoord1  8673  ecopovtrn  8764  f1domg  8915  pw2f1olem  9016  domtriord  9058  mapen  9076  mapxpen  9078  mapunen  9081  nndomog  9144  onomeneq  9145  inficl  9335  supmo  9362  infmo  9407  inf3lem6  9552  cantnflem1  9608  tcmin  9658  tcrank  9806  cardne  9887  cardlim  9894  cardsdomel  9896  carduni  9903  alephord  9995  cardinfima  10017  dfac5lem4  10046  dfac5lem4OLD  10048  infdif2  10129  cofsmo  10189  cfcoflem  10192  infpssrlem4  10226  infpssrlem5  10227  fin4en1  10229  isfin2-2  10239  enfin2i  10241  fin23lem27  10248  isf32lem12  10284  isf34lem6  10300  domtriomlem  10362  cardmin  10484  fpwwe2lem11  10562  inar1  10696  gruiun  10720  ltsonq  10890  prub  10915  reclem3pr  10970  mulcmpblnr  10992  mulgt0sr  11026  axpre-sup  11090  leltadd  11632  infm3  12113  peano5nni  12175  zextle  12600  prime  12608  uzin  12822  ublbneg  12881  zbtwnre  12894  mul2lt0bi  13048  xrre2  13120  xralrple  13155  xmulneg1  13219  supxrbnd  13278  supxrgtmnf  13279  fzrevral  13564  flge  13762  ceile  13806  modadd1  13865  modmul1  13884  modsumfzodifsn  13904  seqcl2  13980  facdiv  14247  hashss  14369  hash2exprb  14431  elfzelfzccat  14540  repswswrd  14744  cshf1  14770  cshwcsh2id  14788  rlim2lt  15457  rlim3  15458  o1lo1  15497  climshftlem  15534  o1co  15546  o1of2  15573  isercolllem2  15626  isercoll  15628  caucvgrlem2  15635  climcndslem2  15813  sqrt2irr  16214  dvds2lem  16235  dvdsle  16277  dvdsfac  16293  ltoddhalfle  16328  divalglem0  16360  ndvdsadd  16377  bitsinv1lem  16408  sadcaddlem  16424  dvdslegcd  16471  bezoutlem2  16507  bezoutlem4  16509  gcdzeq  16519  algcvga  16546  rpdvds  16627  cncongr1  16634  cncongr2  16635  prmind2  16652  isprm6  16682  rpexp  16690  eulerthlem2  16750  pclem  16807  pceulem  16814  pc2dvds  16848  fldivp1  16866  infpnlem1  16879  prmunb  16883  mrieqv2d  17603  plttr  18304  clatl  18472  issubg4  19119  gexdvds  19557  pgpssslw  19587  sylow2alem2  19591  efgs1b  19709  efgsfo  19712  imasabl  19849  lspindpi  21132  psgnodpm  21570  psgndif  21584  obselocv  21710  pf1ind  22348  mdetunilem9  22610  fiinbas  22942  bastg  22956  tgcl  22959  opnssneib  23105  clslp  23138  tgcnp  23243  iscnp4  23253  cncls2  23263  cncls  23264  cnntr  23265  cnpresti  23278  lmss  23288  lmcnp  23294  cmpsub  23390  tgcmp  23391  dfconn2  23409  t1connperf  23426  1stcfb  23435  1stcrest  23443  kgenss  23533  llycmpkgen2  23540  txdis  23622  qtoptop2  23689  kqt0lem  23726  isr0  23727  regr1lem2  23730  cmphaushmeo  23790  fbun  23830  ssfg  23862  fgtr  23880  ufildr  23921  cnpflf  23991  fclsnei  24009  flimfnfcls  24018  fclscmp  24020  ufilcmp  24022  cnpfcf  24031  alexsublem  24034  alexsubALTlem3  24039  alexsubALTlem4  24040  ptcmplem3  24044  tgphaus  24107  tgpt1  24108  tsmsres  24134  imasdsf1olem  24363  xblss2ps  24391  xblss2  24392  blsscls2  24494  metequiv2  24500  stdbdxmet  24505  nmoi  24718  reconn  24819  mulc1cncf  24897  cncfco  24899  iccpnfhmeo  24937  xrhmeo  24938  evth  24951  pi1grplem  25041  fgcfil  25263  ivthlem2  25444  ivthlem3  25445  ovolicc2lem4  25512  voliunlem1  25542  ioombl1lem4  25553  itg2gt0  25752  limcco  25885  lhop1  26006  tdeglem4  26050  plypf1  26202  coeeulem  26214  coeidlem  26227  coeid3  26230  plymul0or  26272  dvnply2  26278  plydivex  26288  vieta1lem2  26302  plyexmo  26304  aaliou3lem2  26334  ulmss  26387  ulmdvlem3  26392  iblulm  26397  sincosq2sgn  26488  sincosq3sgn  26489  sincosq4sgn  26490  logcnlem5  26635  dcubic  26835  amgm  26979  isnsqf  27123  mumullem2  27168  chtublem  27199  chtub  27200  fsumvma2  27202  vmasum  27204  dchrfi  27243  bposlem1  27272  bposlem3  27274  bposlem7  27278  lgsdir  27320  lgsquadlem2  27369  2sqlem8a  27413  2sqlem10  27416  dchrisum0flb  27498  pntpbnd1  27574  pntlemf  27593  pntlem3  27597  addonbday  28296  peano5uzs  28421  axeuclid  29057  uspgrushgr  29271  uspgrupgr  29272  usgruspgr  29274  usgr2pth  29857  crctcshwlkn0lem5  29907  wwlksnext  29986  wwlksnextsurj  29993  clwwlkccatlem  30084  clwlkclwwlkf  30103  clwwisshclwwslemlem  30108  lnon0  30894  normpyc  31242  ocsh  31379  ocorth  31387  ococss  31389  shsel2  31418  hsupss  31437  pjhth  31489  shlub  31510  cm2j  31716  lnfncnbd  32153  riesz1  32161  rnbra  32203  leopadd  32228  leopmuli  32229  hstles  32327  stge1i  32334  stle0i  32335  dmdbr5  32404  ssmd2  32408  superpos  32450  chcv1  32451  atoml2i  32479  chirredlem2  32487  atcvat3i  32492  mdsymlem5  32503  mdsymlem6  32504  sumdmdii  32511  sumdmdlem2  32515  isarchiofld  33287  sqsscirc2  34100  cnre2csqlem  34101  xrge0iifiso  34126  sigaclci  34323  omssubadd  34491  eulerpartlemb  34559  ballotlemimin  34697  ballotlem7  34727  fineqvac  35307  fineqvinfep  35316  vonf1owev  35337  subgrwlk  35361  cusgracyclt3v  35385  cvmlift2lem12  35543  fmlasucdisj  35628  dfon2lem8  36017  segconeq  36239  ifscgr  36273  brofs2  36306  brifs2  36307  endofsegid  36314  dissneqlem  37703  rdgellim  37739  fvineqsneq  37775  tan2h  37980  matunitlindflem2  37985  poimirlem31  38019  poimir  38021  fzmul  38109  fdc  38113  incsequz2  38117  sstotbnd2  38142  sstotbnd3  38144  totbndbnd  38157  isexid2  38223  ispridl2  38406  mpobi123f  38530  disjlem18  39271  disjdmqsss  39273  eldisjs6  39308  riotasvd  39449  lsator0sp  39494  lssatle  39508  lshpset2N  39612  lkrlspeqN  39664  omllaw2N  39737  cmtbr3N  39747  lecmtN  39749  cvlcvr1  39832  cvrval4N  39907  cvrat3  39935  3noncolr2  39942  4noncolr3  39946  3dimlem3  39954  3dimlem3OLDN  39955  3dimlem4  39957  3dimlem4OLDN  39958  llncvrlpln  40051  lplncvrlvol  40109  snatpsubN  40243  linepsubN  40245  pmapjat1  40346  pclfinclN  40443  pl42N  40476  ltrneq2  40641  cdleme7aa  40735  cdleme18d  40788  cdleme21b  40819  trlord  41062  trlcoat  41216  dochkrshp  41879  lcfl8  41995  mulgt0con1dlem  42960  irrapxlem2  43269  pell14qrdich  43315  monotoddzz  43389  pw2f1ocnv  43483  iocinico  43658  ordnexbtwnsuc  43713  tfsconcat0i  43791  naddwordnexlem4  43847  harval3  43983  sbcim2g  44983  stoweidlem62  46506  elfzelfzlble  47785  pgnbgreunbgrlem1  48605  pgnbgreunbgrlem4  48611  1arymaptf1  49134  2arymaptf1  49145  eenglngeehlnmlem2  49230  mpbiran3d  49288  opnneil  49401