Theorem sylan2br 595

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

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

Assertion

Ref	Expression
sylan2br	⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Proof of Theorem sylan2br

Step	Hyp	Ref	Expression
1		sylan2br.1	. . 3 ⊢ (𝜒 ↔ 𝜑)
2	1	biimpri 228	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2br.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 593	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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  df-an 396

This theorem is referenced by:  syl2anbr  599  pm2.61danel  3050  imainss  6143  funeu2  6561  imadif  6619  fnop  6646  ssimaex  6963  tfindsg2  7855  nn0suc  7888  xpexr2  7913  poxp2  8140  sexp3  8150  extmptsuppeq  8185  suppss  8191  suppss2  8197  frrlem14  8296  wfr3g  8319  smores3  8365  tfr3ALT  8414  tz7.48-2  8454  swoso  8751  entrfil  9197  domtrfil  9204  1sdom  9254  isinf  9266  isinfOLD  9267  frfi  9291  dffi3  9441  marypha1lem  9443  ordtypelem7  9536  cnfcom2lem  9713  r1pw  9857  rankxplim3  9893  dfac5  10141  cofsmo  10281  axcclem  10469  zorn2lem7  10514  wloglei  11767  divval  11896  uzind3  12685  xrltnsym  13151  xaddf  13238  xrsupsslem  13321  xrinfmsslem  13322  0fz1  13559  hashunsng  14408  hashunsngx  14409  hashgt0elexb  14418  sumss  15738  fsumss  15739  fsumcvg3  15743  abscvgcvg  15833  isumshft  15853  geoisum1  15893  geoisum1c  15894  mertenslem2  15899  zprod  15951  prodss  15961  fprodss  15962  rpnnen2lem5  16234  gcdcllem3  16518  lcmgcd  16624  lcmdvds  16625  lcmfval  16638  lcmfcl  16645  dvdslcmf  16648  isprm2lem  16698  eulerthlem2  16799  ramcl2lem  17027  imasvscafn  17549  mreexexlem4d  17657  issgrpd  18706  cycsubgcl  19187  galactghm  19383  odlem2  19518  gexlem2  19561  mulgmhm  19806  mulgghm  19807  gsumval3  19886  gsumpt  19941  dprdfeq0  20003  srglmhm  20179  srgrmhm  20180  ringlghm  20270  ringrghm  20271  sdrgacs  20759  cntzsdrg  20760  lssssr  20909  lbsind  21036  cnsubrg  21393  mplmonmul  21992  mplcoe1  21993  mplcoe5  21996  matplusgcell  22369  elcls  23009  neips  23049  opnnei  23056  ordtbaslem  23124  ptclsg  23551  qtopeu  23652  xmetpsmet  24285  comet  24450  metrest  24461  pcorevlem  24975  dyadmbl  25551  mbfeqalem1  25592  i1fadd  25646  itg1addlem2  25648  itg2uba  25694  itgss  25763  dvcnp  25870  quotval  26250  vieta1lem2  26269  aalioulem3  26292  ulmdvlem3  26361  dvradcnv  26380  abelthlem6  26396  abelthlem9  26400  abelth  26401  logtayllem  26618  logtayl  26619  cxpcl  26633  recxpcl  26634  cxpcn3lem  26707  leibpi  26902  musum  27151  dchrelbas3  27199  sumdchr2  27231  lgscllem  27265  lgsdir2  27291  dchrvmasumiflem2  27463  rpvmasum2  27473  padicabv  27591  padicabvf  27592  padicabvcxp  27593  mulsuniflem  28092  divsval  28132  1wlkdlem4  30067  nmooval  30690  hiidge0  31025  hommval  31663  hfmmval  31666  nmcfnlbi  31979  mdslmd1i  32256  mdslmd3i  32259  sumdmdlem2  32346  foresf1o  32431  disjdifprg  32502  xdivval  32839  nsgqusf1olem2  33375  ply1mulrtss  33540  esumfsupre  34048  dya2iocnei  34260  eulerpartlemgc  34340  eulerpartlemb  34346  eulerpartlemgh  34356  ballotlemfc0  34471  ballotlemfcc  34472  subfacp1lem5  35152  subfacp1lem6  35153  cvmliftlem10  35262  elmrsubrn  35488  colinearperm1  36026  colinearperm5  36030  endofsegid  36049  segcon2  36069  seglecgr12im  36074  segletr  36078  colinbtwnle  36082  broutsideof2  36086  btwnoutside  36089  outsideoftr  36093  outsidele  36096  opnbnd  36289  ctbssinf  37370  matunitlindf  37588  poimirlem11  37601  poimirlem12  37602  poimirlem16  37606  poimirlem19  37609  poimirlem26  37616  heibor1lem  37779  heiborlem3  37783  heiborlem10  37790  ablo4pnp  37850  crngm4  37973  lkrpssN  39127  pclvalN  39855  polvalN  39870  lclkrlem2x  41495  hgmaprnlem5N  41865  aks6d1c2p2  42078  unitscyglem2  42155  selvvvval  42555  fsuppssindlem1  42561  infdesc  42613  onsupmaxb  43210  dvgrat  44284  radcnvrat  44286  sswfaxreg  44960  cncfiooicclem1  45870  fourierdlem101  46184  etransclem24  46235  ioorrnopn  46282  isthincd2  49240