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  3048  imainss  6110  funeu2  6516  imadif  6574  fnop  6599  ssimaex  6917  tfindsg2  7802  nn0suc  7834  xpexr2  7859  poxp2  8083  sexp3  8093  extmptsuppeq  8128  suppss  8134  suppss2  8140  frrlem14  8239  wfr3g  8259  smores3  8283  tfr3ALT  8331  tz7.48-2  8371  swoso  8667  entrfil  9107  domtrfil  9114  1sdom  9153  isinf  9163  frfi  9183  dffi3  9332  marypha1lem  9334  ordtypelem7  9427  cnfcom2lem  9608  r1pw  9755  rankxplim3  9791  dfac5  10037  cofsmo  10177  axcclem  10365  zorn2lem7  10410  wloglei  11667  divval  11796  uzind3  12584  xrltnsym  13049  xaddf  13137  xrsupsslem  13220  xrinfmsslem  13221  0fz1  13458  hashunsng  14313  hashunsngx  14314  hashgt0elexb  14323  sumss  15645  fsumss  15646  fsumcvg3  15650  abscvgcvg  15740  isumshft  15760  geoisum1  15800  geoisum1c  15801  mertenslem2  15806  zprod  15858  prodss  15868  fprodss  15869  rpnnen2lem5  16141  gcdcllem3  16426  lcmgcd  16532  lcmdvds  16533  lcmfval  16546  lcmfcl  16553  dvdslcmf  16556  isprm2lem  16606  eulerthlem2  16707  ramcl2lem  16935  imasvscafn  17456  mreexexlem4d  17568  issgrpd  18653  cycsubgcl  19133  galactghm  19331  odlem2  19466  gexlem2  19509  mulgmhm  19754  mulgghm  19755  gsumval3  19834  gsumpt  19889  dprdfeq0  19951  srglmhm  20154  srgrmhm  20155  ringlghm  20245  ringrghm  20246  sdrgacs  20732  cntzsdrg  20733  lssssr  20903  lbsind  21030  cnsubrg  21380  mplmonmul  21989  mplcoe1  21990  mplcoe5  21993  matplusgcell  22375  elcls  23015  neips  23055  opnnei  23062  ordtbaslem  23130  ptclsg  23557  qtopeu  23658  xmetpsmet  24290  comet  24455  metrest  24466  pcorevlem  24980  dyadmbl  25555  mbfeqalem1  25596  i1fadd  25650  itg1addlem2  25652  itg2uba  25698  itgss  25767  dvcnp  25874  quotval  26254  vieta1lem2  26273  aalioulem3  26296  ulmdvlem3  26365  dvradcnv  26384  abelthlem6  26400  abelthlem9  26404  abelth  26405  logtayllem  26622  logtayl  26623  cxpcl  26637  recxpcl  26638  cxpcn3lem  26711  leibpi  26906  musum  27155  dchrelbas3  27203  sumdchr2  27235  lgscllem  27269  lgsdir2  27295  dchrvmasumiflem2  27467  rpvmasum2  27477  padicabv  27595  padicabvf  27596  padicabvcxp  27597  mulsuniflem  28118  divsval  28158  1wlkdlem4  30164  nmooval  30787  hiidge0  31122  hommval  31760  hfmmval  31763  nmcfnlbi  32076  mdslmd1i  32353  mdslmd3i  32356  sumdmdlem2  32443  foresf1o  32528  disjdifprg  32599  xdivval  32949  nsgqusf1olem2  33444  ply1mulrtss  33612  esumfsupre  34177  dya2iocnei  34388  eulerpartlemgc  34468  eulerpartlemb  34474  eulerpartlemgh  34484  ballotlemfc0  34599  ballotlemfcc  34600  subfacp1lem5  35327  subfacp1lem6  35328  cvmliftlem10  35437  elmrsubrn  35663  colinearperm1  36205  colinearperm5  36209  endofsegid  36228  segcon2  36248  seglecgr12im  36253  segletr  36257  colinbtwnle  36261  broutsideof2  36265  btwnoutside  36268  outsideoftr  36272  outsidele  36275  opnbnd  36468  ctbssinf  37550  matunitlindf  37758  poimirlem11  37771  poimirlem12  37772  poimirlem16  37776  poimirlem19  37779  poimirlem26  37786  heibor1lem  37949  heiborlem3  37953  heiborlem10  37960  ablo4pnp  38020  crngm4  38143  lkrpssN  39362  pclvalN  40089  polvalN  40104  lclkrlem2x  41729  hgmaprnlem5N  42099  aks6d1c2p2  42312  unitscyglem2  42389  selvvvval  42770  fsuppssindlem1  42776  infdesc  42828  onsupmaxb  43423  dvgrat  44495  radcnvrat  44497  sswfaxreg  45170  cncfiooicclem1  46079  fourierdlem101  46393  etransclem24  46444  ioorrnopn  46491  isthincd2  49624