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  3057  imainss  6175  funeu2  6593  imadif  6651  fnop  6677  ssimaex  6993  tfindsg2  7882  nn0suc  7916  xpexr2  7941  poxp2  8166  sexp3  8176  extmptsuppeq  8211  suppss  8217  suppss2  8223  frrlem14  8322  wfr3g  8345  smores3  8391  tfr3ALT  8440  tz7.48-2  8480  swoso  8777  entrfil  9222  domtrfil  9229  1sdom  9281  isinf  9293  isinfOLD  9294  frfi  9318  dffi3  9468  marypha1lem  9470  ordtypelem7  9561  cnfcom2lem  9738  r1pw  9882  rankxplim3  9918  dfac5  10166  cofsmo  10306  axcclem  10494  zorn2lem7  10539  wloglei  11792  divval  11921  uzind3  12709  xrltnsym  13175  xaddf  13262  xrsupsslem  13345  xrinfmsslem  13346  0fz1  13580  hashunsng  14427  hashunsngx  14428  hashgt0elexb  14437  sumss  15756  fsumss  15757  fsumcvg3  15761  abscvgcvg  15851  isumshft  15871  geoisum1  15911  geoisum1c  15912  mertenslem2  15917  zprod  15969  prodss  15979  fprodss  15980  rpnnen2lem5  16250  gcdcllem3  16534  lcmgcd  16640  lcmdvds  16641  lcmfval  16654  lcmfcl  16661  dvdslcmf  16664  isprm2lem  16714  eulerthlem2  16815  ramcl2lem  17042  imasvscafn  17583  mreexexlem4d  17691  issgrpd  18755  cycsubgcl  19236  galactghm  19436  odlem2  19571  gexlem2  19614  mulgmhm  19859  mulgghm  19860  gsumval3  19939  gsumpt  19994  dprdfeq0  20056  srglmhm  20238  srgrmhm  20239  ringlghm  20325  ringrghm  20326  sdrgacs  20818  cntzsdrg  20819  lssssr  20969  lbsind  21096  cnsubrg  21462  mplmonmul  22071  mplcoe1  22072  mplcoe5  22075  matplusgcell  22454  elcls  23096  neips  23136  opnnei  23143  ordtbaslem  23211  ptclsg  23638  qtopeu  23739  xmetpsmet  24373  comet  24541  metrest  24552  pcorevlem  25072  dyadmbl  25648  mbfeqalem1  25689  i1fadd  25743  itg1addlem2  25745  itg2uba  25792  itgss  25861  dvcnp  25968  quotval  26348  vieta1lem2  26367  aalioulem3  26390  ulmdvlem3  26459  dvradcnv  26478  abelthlem6  26494  abelthlem9  26498  abelth  26499  logtayllem  26715  logtayl  26716  cxpcl  26730  recxpcl  26731  cxpcn3lem  26804  leibpi  26999  musum  27248  dchrelbas3  27296  sumdchr2  27328  lgscllem  27362  lgsdir2  27388  dchrvmasumiflem2  27560  rpvmasum2  27570  padicabv  27688  padicabvf  27689  padicabvcxp  27690  mulsuniflem  28189  divsval  28229  1wlkdlem4  30168  nmooval  30791  hiidge0  31126  hommval  31764  hfmmval  31767  nmcfnlbi  32080  mdslmd1i  32357  mdslmd3i  32360  sumdmdlem2  32447  foresf1o  32531  disjdifprg  32594  cnvoprabOLD  32737  xdivval  32885  nsgqusf1olem2  33421  ply1mulrtss  33585  esumfsupre  34051  dya2iocnei  34263  eulerpartlemgc  34343  eulerpartlemb  34349  eulerpartlemgh  34359  ballotlemfc0  34473  ballotlemfcc  34474  subfacp1lem5  35168  subfacp1lem6  35169  cvmliftlem10  35278  elmrsubrn  35504  colinearperm1  36043  colinearperm5  36047  endofsegid  36066  segcon2  36086  seglecgr12im  36091  segletr  36095  colinbtwnle  36099  broutsideof2  36103  btwnoutside  36106  outsideoftr  36110  outsidele  36113  opnbnd  36307  ctbssinf  37388  matunitlindf  37604  poimirlem11  37617  poimirlem12  37618  poimirlem16  37622  poimirlem19  37625  poimirlem26  37632  heibor1lem  37795  heiborlem3  37799  heiborlem10  37806  ablo4pnp  37866  crngm4  37989  lkrpssN  39144  pclvalN  39872  polvalN  39887  lclkrlem2x  41512  hgmaprnlem5N  41882  aks6d1c2p2  42100  unitscyglem2  42177  selvvvval  42571  fsuppssindlem1  42577  infdesc  42629  onsupmaxb  43227  dvgrat  44307  radcnvrat  44309  cncfiooicclem1  45848  fourierdlem101  46162  etransclem24  46213  ioorrnopn  46260  isthincd2  48837