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 227	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2br.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 593	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  syl2anbr  599  pm2.61danel  3063  imainss  6051  funeu2  6453  imadif  6511  fnop  6535  ssimaex  6846  tfindsg2  7699  nn0suc  7733  xpexr2  7757  extmptsuppeq  7992  suppss  7998  suppssOLD  7999  suppss2  8004  frrlem14  8103  wfr3g  8126  smores3  8172  tfr3ALT  8221  tz7.48-2  8261  swoso  8519  entrfil  8959  domtrfil  8966  isinf  9024  frfi  9047  dffi3  9178  marypha1lem  9180  ordtypelem7  9271  cnfcom2lem  9447  r1pw  9591  rankxplim3  9627  dfac5  9872  cofsmo  10013  axcclem  10201  zorn2lem7  10246  wloglei  11495  divval  11623  uzind3  12402  xrltnsym  12859  xaddf  12946  xrsupsslem  13029  xrinfmsslem  13030  0fz1  13264  hashunsng  14095  hashunsngx  14096  hashgt0elexb  14105  sumss  15424  fsumss  15425  fsumcvg3  15429  abscvgcvg  15519  isumshft  15539  geoisum1  15579  geoisum1c  15580  mertenslem2  15585  zprod  15635  prodss  15645  fprodss  15646  rpnnen2lem5  15915  gcdcllem3  16196  lcmgcd  16300  lcmdvds  16301  lcmfval  16314  lcmfcl  16321  dvdslcmf  16324  isprm2lem  16374  eulerthlem2  16471  ramcl2lem  16698  imasvscafn  17236  mreexexlem4d  17344  cycsubgcl  18813  galactghm  19000  odlem2  19135  gexlem2  19175  mulgmhm  19417  mulgghm  19418  gsumval3  19496  gsumpt  19551  dprdfeq0  19613  srglmhm  19759  srgrmhm  19760  ringlghm  19831  ringrghm  19832  sdrgacs  20057  cntzsdrg  20058  lssssr  20203  lbsind  20330  cnsubrg  20646  mplmonmul  21225  mplcoe1  21226  mplcoe5  21229  matplusgcell  21570  elcls  22212  neips  22252  opnnei  22259  ordtbaslem  22327  ptclsg  22754  qtopeu  22855  xmetpsmet  23489  comet  23657  metrest  23668  pcorevlem  24177  dyadmbl  24752  mbfeqalem1  24793  i1fadd  24847  itg1addlem2  24849  itg2uba  24896  itgss  24964  dvcnp  25071  quotval  25440  vieta1lem2  25459  aalioulem3  25482  ulmdvlem3  25549  dvradcnv  25568  abelthlem6  25583  abelthlem9  25587  abelth  25588  logtayllem  25802  logtayl  25803  cxpcl  25817  recxpcl  25818  cxpcn3lem  25888  leibpi  26080  musum  26328  dchrelbas3  26374  sumdchr2  26406  lgscllem  26440  lgsdir2  26466  dchrvmasumiflem2  26638  rpvmasum2  26648  padicabv  26766  padicabvf  26767  padicabvcxp  26768  1wlkdlem4  28490  nmooval  29111  hiidge0  29446  hommval  30084  hfmmval  30087  nmcfnlbi  30400  mdslmd1i  30677  mdslmd3i  30680  sumdmdlem2  30767  foresf1o  30836  disjdifprg  30900  cnvoprabOLD  31041  xdivval  31179  nsgqusf1olem2  31585  esumfsupre  32025  dya2iocnei  32235  eulerpartlemgc  32315  eulerpartlemb  32321  eulerpartlemgh  32331  ballotlemfc0  32445  ballotlemfcc  32446  subfacp1lem5  33132  subfacp1lem6  33133  cvmliftlem10  33242  elmrsubrn  33468  poxp2  33776  xpord3pred  33784  sexp3  33785  colinearperm1  34350  colinearperm5  34354  endofsegid  34373  segcon2  34393  seglecgr12im  34398  segletr  34402  colinbtwnle  34406  broutsideof2  34410  btwnoutside  34413  outsideoftr  34417  outsidele  34420  opnbnd  34500  ctbssinf  35563  matunitlindf  35761  poimirlem11  35774  poimirlem12  35775  poimirlem16  35779  poimirlem19  35782  poimirlem26  35789  heibor1lem  35953  heiborlem3  35957  heiborlem10  35964  ablo4pnp  36024  crngm4  36147  lkrpssN  37163  pclvalN  37890  polvalN  37905  lclkrlem2x  39530  hgmaprnlem5N  39900  fsuppssindlem1  40266  infdesc  40466  dvgrat  41889  radcnvrat  41891  cncfiooicclem1  43393  fourierdlem101  43707  etransclem24  43758  ioorrnopn  43805  isthincd2  46275