Theorem sylan2br 607

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 605	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  syl2anbr  611  pm2.61danel  3079  imainss  6150  funeu2  6575  imadif  6635  fnop  6659  ssimaex  6981  tfindsg2  7883  nn0suc  7916  xpexr2  7941  poxp2  8173  sexp3  8183  extmptsuppeq  8219  suppss  8225  suppss2  8231  frrlem14  8331  wfr3g  8351  smores3  8375  tfr3ALT  8424  tz7.48-2  8466  swoso  8766  entrfil  9214  domtrfil  9221  1sdom  9260  isinf  9270  frfi  9290  dffi3  9436  marypha1lem  9438  ordtypelem7  9531  cnfcom2lem  9715  r1pw  9872  rankxplim3  9911  dfac5  10220  cofsmo  10360  axcclem  10548  zorn2lem7  10593  wloglei  11861  divval  11989  uzind3  12806  xrltnsym  13279  xaddf  13367  xrsupsslem  13450  xrinfmsslem  13451  0fz1  13690  hashunsng  14549  hashunsngx  14550  hashgt0elexb  14559  sumss  15905  fsumss  15906  fsumcvg3  15910  abscvgcvg  16001  isumshft  16023  geoisum1  16063  geoisum1c  16064  mertenslem2  16069  zprod  16119  prodss  16129  fprodss  16130  rpnnen2lem5  16401  gcdcllem3  16686  lcmgcd  16797  lcmdvds  16798  lcmfval  16811  lcmfcl  16818  dvdslcmf  16821  isprm2lem  16871  eulerthlem2  16974  ramcl2lem  17202  imasvscafn  17724  mreexexlem4d  17836  issgrpd  18934  cycsubgcl  19436  galactghm  19633  odlem2  19768  gexlem2  19811  mulgmhm  20056  mulgghm  20057  gsumval3  20136  gsumpt  20191  dprdfeq0  20253  srglmhm  20462  srgrmhm  20463  ringlghm  20558  ringrghm  20559  sdrgacs  21073  cntzsdrg  21074  lssssr  21244  lbsind  21370  cnsubrg  21748  mplmonmul  22360  mplcoe1  22361  mplcoe5  22364  selvvvval  22466  matplusgcell  22763  matunitlindf  23011  elcls  23406  neips  23446  opnnei  23453  ordtbaslem  23521  ptclsg  23949  qtopeu  24050  xmetpsmet  24682  comet  24847  metrest  24858  pcorevlem  25362  dyadmbl  25936  mbfeqalem1  25977  i1fadd  26031  itg1addlem2  26033  itg2uba  26079  itgss  26147  dvcnp  26254  quotval  26628  vieta1lem2  26649  aalioulem3  26676  ulmdvlem3  26744  dvradcnv  26763  abelthlem6  26778  abelthlem9  26782  abelth  26783  logtayllem  27002  logtayl  27003  cxpcl  27017  recxpcl  27018  cxpcn3lem  27090  leibpi  27285  musum  27533  dchrelbas3  27580  sumdchr2  27612  lgscllem  27646  lgsdir2  27672  dchrvmasumiflem2  27844  rpvmasum2  27854  padicabv  27972  padicabvf  27973  padicabvcxp  27974  infdesc  27982  mulsuniflem  28550  divsval  28590  1wlkdlem4  30746  nmooval  31380  hiidge0  31715  hommval  32353  hfmmval  32356  nmcfnlbi  32669  mdslmd1i  32946  mdslmd3i  32949  sumdmdlem2  33036  foresf1o  33157  disjdifprg  33226  xdivval  33541  nsgqusf1olem2  34021  ply1mulrtss  34170  psrmonmul  34238  esumfsupre  34759  dya2iocnei  34970  eulerpartlemgc  35050  eulerpartlemb  35056  eulerpartlemgh  35066  ballotlemfc0  35181  ballotlemfcc  35182  fnlfvk3n0  35985  subfacp1lem5  36073  subfacp1lem6  36074  cvmliftlem10  36183  elmrsubrn  36409  elpssmo  36591  colinearperm1  36960  colinearperm5  36964  endofsegid  36983  segcon2  37003  seglecgr12im  37008  segletr  37012  colinbtwnle  37016  broutsideof2  37020  btwnoutside  37023  outsideoftr  37027  outsidele  37030  opnbnd  37246  ctbssinf  38475  poimirlem11  38695  poimirlem12  38696  poimirlem16  38700  poimirlem19  38703  poimirlem26  38710  heibor1lem  38889  heiborlem3  38893  heiborlem10  38900  ablo4pnp  38960  crngm4  39083  lkrpssN  40366  pclvalN  41093  polvalN  41108  lclkrlem2x  42733  hgmaprnlem5N  43103  aks6d1c2p2  43315  unitscyglem2  43392  fsuppssindlem1  43765  onsupmaxb  44387  dvgrat  45442  radcnvrat  45444  sswfaxreg  46122  cncfiooicclem1  47048  fourierdlem101  47362  etransclem24  47413  ioorrnopn  47460  indprm  48859  isthincd2  50717