Theorem sylan2br 606

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  syl2anbr  610  pm2.61danel  3084  imainss  6152  funeu2  6563  imadif  6621  fnop  6645  ssimaex  6967  tfindsg2  7858  nn0suc  7891  xpexr2  7916  poxp2  8139  sexp3  8149  extmptsuppeq  8184  suppss  8190  suppss2  8196  frrlem14  8296  wfr3g  8316  smores3  8340  tfr3ALT  8389  tz7.48-2  8429  swoso  8729  entrfil  9169  domtrfil  9176  1sdom  9215  isinf  9225  frfi  9245  dffi3  9391  marypha1lem  9393  ordtypelem7  9486  cnfcom2lem  9670  r1pw  9817  rankxplim3  9853  dfac5  10112  cofsmo  10253  axcclem  10441  zorn2lem7  10486  wloglei  11746  divval  11874  uzind3  12690  xrltnsym  13162  xaddf  13250  xrsupsslem  13333  xrinfmsslem  13334  0fz1  13572  hashunsng  14428  hashunsngx  14429  hashgt0elexb  14438  sumss  15775  fsumss  15776  fsumcvg3  15780  abscvgcvg  15871  isumshft  15893  geoisum1  15933  geoisum1c  15934  mertenslem2  15939  zprod  15991  prodss  16001  fprodss  16002  rpnnen2lem5  16274  gcdcllem3  16559  lcmgcd  16665  lcmdvds  16666  lcmfval  16679  lcmfcl  16686  dvdslcmf  16689  isprm2lem  16739  eulerthlem2  16841  ramcl2lem  17069  imasvscafn  17591  mreexexlem4d  17703  issgrpd  18788  cycsubgcl  19277  galactghm  19474  odlem2  19609  gexlem2  19652  mulgmhm  19897  mulgghm  19898  gsumval3  19977  gsumpt  20032  dprdfeq0  20094  srglmhm  20303  srgrmhm  20304  ringlghm  20395  ringrghm  20396  sdrgacs  20882  cntzsdrg  20883  lssssr  21053  lbsind  21179  cnsubrg  21546  mplmonmul  22156  mplcoe1  22157  mplcoe5  22160  selvvvval  22262  matplusgcell  22559  elcls  23199  neips  23239  opnnei  23246  ordtbaslem  23314  ptclsg  23741  qtopeu  23842  xmetpsmet  24474  comet  24639  metrest  24650  pcorevlem  25154  dyadmbl  25728  mbfeqalem1  25769  i1fadd  25823  itg1addlem2  25825  itg2uba  25871  itgss  25940  dvcnp  26047  quotval  26422  vieta1lem2  26441  aalioulem3  26464  ulmdvlem3  26531  dvradcnv  26550  abelthlem6  26565  abelthlem9  26569  abelth  26570  logtayllem  26790  logtayl  26791  cxpcl  26805  recxpcl  26806  cxpcn3lem  26878  leibpi  27073  musum  27321  dchrelbas3  27368  sumdchr2  27400  lgscllem  27434  lgsdir2  27460  dchrvmasumiflem2  27632  rpvmasum2  27642  padicabv  27760  padicabvf  27761  padicabvcxp  27762  mulsuniflem  28308  divsval  28348  1wlkdlem4  30432  nmooval  31056  hiidge0  31391  hommval  32029  hfmmval  32032  nmcfnlbi  32345  mdslmd1i  32622  mdslmd3i  32625  sumdmdlem2  32712  foresf1o  32791  disjdifprg  32861  xdivval  33179  nsgqusf1olem2  33667  ply1mulrtss  33817  psrmonmul  33885  esumfsupre  34406  dya2iocnei  34617  eulerpartlemgc  34697  eulerpartlemb  34703  eulerpartlemgh  34713  ballotlemfc0  34828  ballotlemfcc  34829  subfacp1lem5  35609  subfacp1lem6  35610  cvmliftlem10  35719  elmrsubrn  35945  colinearperm1  36487  colinearperm5  36491  endofsegid  36510  segcon2  36530  seglecgr12im  36535  segletr  36539  colinbtwnle  36543  broutsideof2  36547  btwnoutside  36550  outsideoftr  36554  outsidele  36557  opnbnd  36759  ctbssinf  37974  matunitlindf  38191  poimirlem11  38204  poimirlem12  38205  poimirlem16  38209  poimirlem19  38212  poimirlem26  38219  heibor1lem  38382  heiborlem3  38386  heiborlem10  38393  ablo4pnp  38453  crngm4  38576  lkrpssN  39861  pclvalN  40588  polvalN  40603  lclkrlem2x  42228  hgmaprnlem5N  42598  aks6d1c2p2  42810  unitscyglem2  42887  fsuppssindlem1  43249  infdesc  43301  onsupmaxb  43892  dvgrat  44948  radcnvrat  44950  sswfaxreg  45622  cncfiooicclem1  46533  fourierdlem101  46847  etransclem24  46898  ioorrnopn  46945  indprm  48304  isthincd2  50134