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  3043  imainss  6103  funeu2  6508  imadif  6566  fnop  6591  ssimaex  6908  tfindsg2  7795  nn0suc  7827  xpexr2  7852  poxp2  8076  sexp3  8086  extmptsuppeq  8121  suppss  8127  suppss2  8133  frrlem14  8232  wfr3g  8252  smores3  8276  tfr3ALT  8324  tz7.48-2  8364  swoso  8659  entrfil  9099  domtrfil  9106  1sdom  9144  isinf  9154  frfi  9174  dffi3  9321  marypha1lem  9323  ordtypelem7  9416  cnfcom2lem  9597  r1pw  9741  rankxplim3  9777  dfac5  10023  cofsmo  10163  axcclem  10351  zorn2lem7  10396  wloglei  11652  divval  11781  uzind3  12570  xrltnsym  13039  xaddf  13126  xrsupsslem  13209  xrinfmsslem  13210  0fz1  13447  hashunsng  14299  hashunsngx  14300  hashgt0elexb  14309  sumss  15631  fsumss  15632  fsumcvg3  15636  abscvgcvg  15726  isumshft  15746  geoisum1  15786  geoisum1c  15787  mertenslem2  15792  zprod  15844  prodss  15854  fprodss  15855  rpnnen2lem5  16127  gcdcllem3  16412  lcmgcd  16518  lcmdvds  16519  lcmfval  16532  lcmfcl  16539  dvdslcmf  16542  isprm2lem  16592  eulerthlem2  16693  ramcl2lem  16921  imasvscafn  17441  mreexexlem4d  17553  issgrpd  18604  cycsubgcl  19085  galactghm  19283  odlem2  19418  gexlem2  19461  mulgmhm  19706  mulgghm  19707  gsumval3  19786  gsumpt  19841  dprdfeq0  19903  srglmhm  20106  srgrmhm  20107  ringlghm  20197  ringrghm  20198  sdrgacs  20686  cntzsdrg  20687  lssssr  20857  lbsind  20984  cnsubrg  21334  mplmonmul  21941  mplcoe1  21942  mplcoe5  21945  matplusgcell  22318  elcls  22958  neips  22998  opnnei  23005  ordtbaslem  23073  ptclsg  23500  qtopeu  23601  xmetpsmet  24234  comet  24399  metrest  24410  pcorevlem  24924  dyadmbl  25499  mbfeqalem1  25540  i1fadd  25594  itg1addlem2  25596  itg2uba  25642  itgss  25711  dvcnp  25818  quotval  26198  vieta1lem2  26217  aalioulem3  26240  ulmdvlem3  26309  dvradcnv  26328  abelthlem6  26344  abelthlem9  26348  abelth  26349  logtayllem  26566  logtayl  26567  cxpcl  26581  recxpcl  26582  cxpcn3lem  26655  leibpi  26850  musum  27099  dchrelbas3  27147  sumdchr2  27179  lgscllem  27213  lgsdir2  27239  dchrvmasumiflem2  27411  rpvmasum2  27421  padicabv  27539  padicabvf  27540  padicabvcxp  27541  mulsuniflem  28057  divsval  28097  1wlkdlem4  30084  nmooval  30707  hiidge0  31042  hommval  31680  hfmmval  31683  nmcfnlbi  31996  mdslmd1i  32273  mdslmd3i  32276  sumdmdlem2  32363  foresf1o  32448  disjdifprg  32519  xdivval  32860  nsgqusf1olem2  33352  ply1mulrtss  33518  esumfsupre  34044  dya2iocnei  34256  eulerpartlemgc  34336  eulerpartlemb  34342  eulerpartlemgh  34352  ballotlemfc0  34467  ballotlemfcc  34468  subfacp1lem5  35167  subfacp1lem6  35168  cvmliftlem10  35277  elmrsubrn  35503  colinearperm1  36046  colinearperm5  36050  endofsegid  36069  segcon2  36089  seglecgr12im  36094  segletr  36098  colinbtwnle  36102  broutsideof2  36106  btwnoutside  36109  outsideoftr  36113  outsidele  36116  opnbnd  36309  ctbssinf  37390  matunitlindf  37608  poimirlem11  37621  poimirlem12  37622  poimirlem16  37626  poimirlem19  37629  poimirlem26  37636  heibor1lem  37799  heiborlem3  37803  heiborlem10  37810  ablo4pnp  37870  crngm4  37993  lkrpssN  39152  pclvalN  39879  polvalN  39894  lclkrlem2x  41519  hgmaprnlem5N  41889  aks6d1c2p2  42102  unitscyglem2  42179  selvvvval  42568  fsuppssindlem1  42574  infdesc  42626  onsupmaxb  43222  dvgrat  44295  radcnvrat  44297  sswfaxreg  44971  cncfiooicclem1  45884  fourierdlem101  46198  etransclem24  46249  ioorrnopn  46296  isthincd2  49432