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  opeldmd  5875  elreldm  5904  predtrss  6298  ordtr2  6380  ssimaex  6941  fliftfun  7285  isopolem  7318  isosolem  7320  ordsucss  7787  f1oweALT  7942  fnse  8101  soseq  8127  brtpos  8203  issmo2  8308  seqomlem1  8409  omcl  8493  oecl  8494  oawordeulem  8511  oaass  8518  omordi  8523  omord  8525  odi  8536  oen0  8544  oeordi  8545  oeordsuc  8552  nnmcl  8570  nnecl  8571  nnmordi  8589  nnmord  8590  nnmwordri  8594  nnaordex  8596  swoord1  8699  ecopovtrn  8790  f1domg  8941  pw2f1olem  9042  domtriord  9084  mapen  9102  mapxpen  9104  mapunen  9107  nndomog  9170  onomeneq  9171  inficl  9361  supmo  9388  infmo  9433  inf3lem6  9578  cantnflem1  9634  tcmin  9684  tcrank  9832  cardne  9913  cardlim  9920  cardsdomel  9922  carduni  9929  alephord  10021  cardinfima  10043  dfac5lem4  10072  dfac5lem4OLD  10074  infdif2  10155  cofsmo  10216  cfcoflem  10219  infpssrlem4  10253  infpssrlem5  10254  fin4en1  10256  isfin2-2  10266  enfin2i  10268  fin23lem27  10275  isf32lem12  10311  isf34lem6  10327  domtriomlem  10389  cardmin  10511  fpwwe2lem11  10589  inar1  10723  gruiun  10747  ltsonq  10917  prub  10942  reclem3pr  10997  mulcmpblnr  11019  mulgt0sr  11053  axpre-sup  11117  leltadd  11661  infm3  12141  peano5nni  12203  zextle  12636  prime  12644  uzin  12865  ublbneg  12924  zbtwnre  12937  mul2lt0bi  13091  xrre2  13163  xralrple  13198  xmulneg1  13262  supxrbnd  13321  supxrgtmnf  13322  fzrevral  13607  flge  13805  ceile  13849  modadd1  13908  modmul1  13927  modsumfzodifsn  13947  seqcl2  14023  facdiv  14290  hashss  14412  hash2exprb  14474  elfzelfzccat  14583  repswswrd  14787  cshf1  14813  cshwcsh2id  14831  rlim2lt  15500  rlim3  15501  o1lo1  15540  climshftlem  15577  o1co  15589  o1of2  15616  isercolllem2  15669  isercoll  15671  caucvgrlem2  15678  climcndslem2  15856  sqrt2irr  16257  dvds2lem  16278  dvdsle  16320  dvdsfac  16336  ltoddhalfle  16371  divalglem0  16403  ndvdsadd  16420  bitsinv1lem  16451  sadcaddlem  16467  dvdslegcd  16514  bezoutlem2  16550  bezoutlem4  16552  gcdzeq  16562  algcvga  16589  rpdvds  16670  cncongr1  16677  cncongr2  16678  prmind2  16695  isprm6  16725  rpexp  16733  eulerthlem2  16793  pclem  16850  pceulem  16857  pc2dvds  16891  fldivp1  16909  infpnlem1  16922  prmunb  16926  mrieqv2d  17647  plttr  18348  clatl  18516  issubg4  19163  gexdvds  19600  pgpssslw  19630  sylow2alem2  19634  efgs1b  19752  efgsfo  19755  imasabl  19892  lspindpi  21175  psgnodpm  21613  psgndif  21627  obselocv  21753  pf1ind  22391  mdetunilem9  22653  fiinbas  22985  bastg  22999  tgcl  23002  opnssneib  23148  clslp  23181  tgcnp  23286  iscnp4  23296  cncls2  23306  cncls  23307  cnntr  23308  cnpresti  23321  lmss  23331  lmcnp  23337  cmpsub  23433  tgcmp  23434  dfconn2  23452  t1connperf  23469  1stcfb  23478  1stcrest  23486  kgenss  23576  llycmpkgen2  23583  txdis  23665  qtoptop2  23732  kqt0lem  23769  isr0  23770  regr1lem2  23773  cmphaushmeo  23833  fbun  23873  ssfg  23905  fgtr  23923  ufildr  23964  cnpflf  24034  fclsnei  24052  flimfnfcls  24061  fclscmp  24063  ufilcmp  24065  cnpfcf  24074  alexsublem  24077  alexsubALTlem3  24082  alexsubALTlem4  24083  ptcmplem3  24087  tgphaus  24150  tgpt1  24151  tsmsres  24177  imasdsf1olem  24406  xblss2ps  24434  xblss2  24435  blsscls2  24537  metequiv2  24543  stdbdxmet  24548  nmoi  24761  reconn  24862  mulc1cncf  24940  cncfco  24942  iccpnfhmeo  24980  xrhmeo  24981  evth  24994  pi1grplem  25084  fgcfil  25306  ivthlem2  25487  ivthlem3  25488  ovolicc2lem4  25555  voliunlem1  25585  ioombl1lem4  25596  itg2gt0  25795  limcco  25928  lhop1  26049  tdeglem4  26093  plypf1  26245  coeeulem  26257  coeidlem  26270  coeid3  26273  plymul0or  26315  dvnply2  26321  plydivex  26331  vieta1lem2  26345  plyexmo  26347  aaliou3lem2  26377  ulmss  26430  ulmdvlem3  26435  iblulm  26440  sincosq2sgn  26534  sincosq3sgn  26535  sincosq4sgn  26536  logcnlem5  26681  dcubic  26881  amgm  27025  isnsqf  27169  mumullem2  27214  chtublem  27245  chtub  27246  fsumvma2  27248  vmasum  27250  dchrfi  27289  bposlem1  27318  bposlem3  27320  bposlem7  27324  lgsdir  27366  lgsquadlem2  27415  2sqlem8a  27459  2sqlem10  27462  dchrisum0flb  27544  pntpbnd1  27620  pntlemf  27639  pntlem3  27643  addonbday  28342  peano5uzs  28467  axeuclid  29103  uspgrushgr  29317  uspgrupgr  29318  usgruspgr  29320  usgr2pth  29903  crctcshwlkn0lem5  29953  wwlksnext  30032  wwlksnextsurj  30039  clwwlkccatlem  30130  clwlkclwwlkf  30149  clwwisshclwwslemlem  30154  lnon0  30940  normpyc  31288  ocsh  31425  ocorth  31433  ococss  31435  shsel2  31464  hsupss  31483  pjhth  31535  shlub  31556  cm2j  31762  lnfncnbd  32199  riesz1  32207  rnbra  32249  leopadd  32274  leopmuli  32275  hstles  32373  stge1i  32380  stle0i  32381  dmdbr5  32450  ssmd2  32454  superpos  32496  chcv1  32497  atoml2i  32525  chirredlem2  32533  atcvat3i  32538  mdsymlem5  32549  mdsymlem6  32550  sumdmdii  32557  sumdmdlem2  32561  isarchiofld  33333  sqsscirc2  34160  cnre2csqlem  34161  xrge0iifiso  34186  sigaclci  34383  omssubadd  34551  eulerpartlemb  34619  ballotlemimin  34757  ballotlem7  34787  fineqvac  35367  fineqvinfep  35376  vonf1owev  35406  subgrwlk  35430  cusgracyclt3v  35454  cvmlift2lem12  35612  fmlasucdisj  35697  dfon2lem8  36086  segconeq  36308  ifscgr  36342  brofs2  36375  brifs2  36376  endofsegid  36383  dissneqlem  37782  rdgellim  37818  fvineqsneq  37854  tan2h  38059  matunitlindflem2  38064  poimirlem31  38098  poimir  38100  fzmul  38188  fdc  38192  incsequz2  38196  sstotbnd2  38221  sstotbnd3  38223  totbndbnd  38236  isexid2  38302  ispridl2  38485  mpobi123f  38609  disjlem18  39350  disjdmqsss  39352  eldisjs6  39387  riotasvd  39528  lsator0sp  39573  lssatle  39587  lshpset2N  39691  lkrlspeqN  39743  omllaw2N  39816  cmtbr3N  39826  lecmtN  39828  cvlcvr1  39911  cvrval4N  39986  cvrat3  40014  3noncolr2  40021  4noncolr3  40025  3dimlem3  40033  3dimlem3OLDN  40034  3dimlem4  40036  3dimlem4OLDN  40037  llncvrlpln  40130  lplncvrlvol  40188  snatpsubN  40322  linepsubN  40324  pmapjat1  40425  pclfinclN  40522  pl42N  40555  ltrneq2  40720  cdleme7aa  40814  cdleme18d  40867  cdleme21b  40898  trlord  41141  trlcoat  41295  dochkrshp  41958  lcfl8  42074  mulgt0con1dlem  43039  irrapxlem2  43348  pell14qrdich  43394  monotoddzz  43468  pw2f1ocnv  43562  iocinico  43737  ordnexbtwnsuc  43792  tfsconcat0i  43870  naddwordnexlem4  43926  harval3  44062  sbcim2g  45062  stoweidlem62  46584  elfzelfzlble  47863  pgnbgreunbgrlem1  48683  pgnbgreunbgrlem4  48689  1arymaptf1  49212  2arymaptf1  49223  eenglngeehlnmlem2  49308  mpbiran3d  49366  opnneil  49479