Theorem sylan2br 596

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 594	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  600  pm2.61danel  3051  imainss  6114  funeu2  6520  imadif  6578  fnop  6603  ssimaex  6921  tfindsg2  7808  nn0suc  7840  xpexr2  7865  poxp2  8088  sexp3  8098  extmptsuppeq  8133  suppss  8139  suppss2  8145  frrlem14  8244  wfr3g  8264  smores3  8288  tfr3ALT  8336  tz7.48-2  8376  swoso  8673  entrfil  9114  domtrfil  9121  1sdom  9160  isinf  9170  frfi  9190  dffi3  9339  marypha1lem  9341  ordtypelem7  9434  cnfcom2lem  9617  r1pw  9764  rankxplim3  9800  dfac5  10046  cofsmo  10186  axcclem  10374  zorn2lem7  10419  wloglei  11677  divval  11806  uzind3  12618  xrltnsym  13083  xaddf  13171  xrsupsslem  13254  xrinfmsslem  13255  0fz1  13493  hashunsng  14349  hashunsngx  14350  hashgt0elexb  14359  sumss  15681  fsumss  15682  fsumcvg3  15686  abscvgcvg  15777  isumshft  15799  geoisum1  15839  geoisum1c  15840  mertenslem2  15845  zprod  15897  prodss  15907  fprodss  15908  rpnnen2lem5  16180  gcdcllem3  16465  lcmgcd  16571  lcmdvds  16572  lcmfval  16585  lcmfcl  16592  dvdslcmf  16595  isprm2lem  16645  eulerthlem2  16747  ramcl2lem  16975  imasvscafn  17496  mreexexlem4d  17608  issgrpd  18693  cycsubgcl  19176  galactghm  19374  odlem2  19509  gexlem2  19552  mulgmhm  19797  mulgghm  19798  gsumval3  19877  gsumpt  19932  dprdfeq0  19994  srglmhm  20197  srgrmhm  20198  ringlghm  20288  ringrghm  20289  sdrgacs  20773  cntzsdrg  20774  lssssr  20944  lbsind  21071  cnsubrg  21421  mplmonmul  22028  mplcoe1  22029  mplcoe5  22032  matplusgcell  22412  elcls  23052  neips  23092  opnnei  23099  ordtbaslem  23167  ptclsg  23594  qtopeu  23695  xmetpsmet  24327  comet  24492  metrest  24503  pcorevlem  25007  dyadmbl  25581  mbfeqalem1  25622  i1fadd  25676  itg1addlem2  25678  itg2uba  25724  itgss  25793  dvcnp  25900  quotval  26273  vieta1lem2  26292  aalioulem3  26315  ulmdvlem3  26384  dvradcnv  26403  abelthlem6  26418  abelthlem9  26422  abelth  26423  logtayllem  26640  logtayl  26641  cxpcl  26655  recxpcl  26656  cxpcn3lem  26728  leibpi  26923  musum  27172  dchrelbas3  27219  sumdchr2  27251  lgscllem  27285  lgsdir2  27311  dchrvmasumiflem2  27483  rpvmasum2  27493  padicabv  27611  padicabvf  27612  padicabvcxp  27613  mulsuniflem  28159  divsval  28199  1wlkdlem4  30229  nmooval  30853  hiidge0  31188  hommval  31826  hfmmval  31829  nmcfnlbi  32142  mdslmd1i  32419  mdslmd3i  32422  sumdmdlem2  32509  foresf1o  32593  disjdifprg  32664  xdivval  32997  nsgqusf1olem2  33493  ply1mulrtss  33661  psrmonmul  33713  esumfsupre  34235  dya2iocnei  34446  eulerpartlemgc  34526  eulerpartlemb  34532  eulerpartlemgh  34542  ballotlemfc0  34657  ballotlemfcc  34658  subfacp1lem5  35386  subfacp1lem6  35387  cvmliftlem10  35496  elmrsubrn  35722  colinearperm1  36264  colinearperm5  36268  endofsegid  36287  segcon2  36307  seglecgr12im  36312  segletr  36316  colinbtwnle  36320  broutsideof2  36324  btwnoutside  36327  outsideoftr  36331  outsidele  36334  opnbnd  36527  ctbssinf  37740  matunitlindf  37957  poimirlem11  37970  poimirlem12  37971  poimirlem16  37975  poimirlem19  37978  poimirlem26  37985  heibor1lem  38148  heiborlem3  38152  heiborlem10  38159  ablo4pnp  38219  crngm4  38342  lkrpssN  39627  pclvalN  40354  polvalN  40369  lclkrlem2x  41994  hgmaprnlem5N  42364  aks6d1c2p2  42576  unitscyglem2  42653  selvvvval  43036  fsuppssindlem1  43042  infdesc  43094  onsupmaxb  43689  dvgrat  44761  radcnvrat  44763  sswfaxreg  45436  cncfiooicclem1  46343  fourierdlem101  46657  etransclem24  46708  ioorrnopn  46755  indprm  48108  isthincd2  49928