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  3076  imainss  6144  funeu2  6566  imadif  6624  fnop  6648  ssimaex  6970  tfindsg2  7873  nn0suc  7906  xpexr2  7931  poxp2  8160  sexp3  8170  extmptsuppeq  8205  suppss  8211  suppss2  8217  frrlem14  8317  wfr3g  8337  smores3  8361  tfr3ALT  8410  tz7.48-2  8452  swoso  8752  entrfil  9200  domtrfil  9207  1sdom  9246  isinf  9256  frfi  9276  dffi3  9423  marypha1lem  9425  ordtypelem7  9518  cnfcom2lem  9702  r1pw  9859  rankxplim3  9898  dfac5  10207  cofsmo  10347  axcclem  10535  zorn2lem7  10580  wloglei  11848  divval  11976  uzind3  12793  xrltnsym  13266  xaddf  13354  xrsupsslem  13437  xrinfmsslem  13438  0fz1  13677  hashunsng  14536  hashunsngx  14537  hashgt0elexb  14546  sumss  15890  fsumss  15891  fsumcvg3  15895  abscvgcvg  15986  isumshft  16008  geoisum1  16048  geoisum1c  16049  mertenslem2  16054  zprod  16104  prodss  16114  fprodss  16115  rpnnen2lem5  16386  gcdcllem3  16671  lcmgcd  16782  lcmdvds  16783  lcmfval  16796  lcmfcl  16803  dvdslcmf  16806  isprm2lem  16856  eulerthlem2  16959  ramcl2lem  17187  imasvscafn  17709  mreexexlem4d  17821  issgrpd  18919  cycsubgcl  19421  galactghm  19618  odlem2  19753  gexlem2  19796  mulgmhm  20041  mulgghm  20042  gsumval3  20121  gsumpt  20176  dprdfeq0  20238  srglmhm  20447  srgrmhm  20448  ringlghm  20543  ringrghm  20544  sdrgacs  21058  cntzsdrg  21059  lssssr  21229  lbsind  21355  cnsubrg  21733  mplmonmul  22345  mplcoe1  22346  mplcoe5  22349  selvvvval  22451  matplusgcell  22748  matunitlindf  22996  elcls  23391  neips  23431  opnnei  23438  ordtbaslem  23506  ptclsg  23934  qtopeu  24035  xmetpsmet  24667  comet  24832  metrest  24843  pcorevlem  25347  dyadmbl  25921  mbfeqalem1  25962  i1fadd  26016  itg1addlem2  26018  itg2uba  26064  itgss  26132  dvcnp  26239  quotval  26613  vieta1lem2  26634  aalioulem3  26661  ulmdvlem3  26729  dvradcnv  26748  abelthlem6  26763  abelthlem9  26767  abelth  26768  logtayllem  26987  logtayl  26988  cxpcl  27002  recxpcl  27003  cxpcn3lem  27075  leibpi  27270  musum  27518  dchrelbas3  27565  sumdchr2  27597  lgscllem  27631  lgsdir2  27657  dchrvmasumiflem2  27829  rpvmasum2  27839  padicabv  27957  padicabvf  27958  padicabvcxp  27959  infdesc  27967  mulsuniflem  28535  divsval  28575  1wlkdlem4  30731  nmooval  31365  hiidge0  31700  hommval  32338  hfmmval  32341  nmcfnlbi  32654  mdslmd1i  32931  mdslmd3i  32934  sumdmdlem2  33021  foresf1o  33100  disjdifprg  33169  xdivval  33485  nsgqusf1olem2  33965  ply1mulrtss  34114  psrmonmul  34182  esumfsupre  34703  dya2iocnei  34914  eulerpartlemgc  34994  eulerpartlemb  35000  eulerpartlemgh  35010  ballotlemfc0  35125  ballotlemfcc  35126  subfacp1lem5  35949  subfacp1lem6  35950  cvmliftlem10  36059  elmrsubrn  36285  colinearperm1  36827  colinearperm5  36831  endofsegid  36850  segcon2  36870  seglecgr12im  36875  segletr  36879  colinbtwnle  36883  broutsideof2  36887  btwnoutside  36890  outsideoftr  36894  outsidele  36897  opnbnd  37113  ctbssinf  38329  poimirlem11  38549  poimirlem12  38550  poimirlem16  38554  poimirlem19  38557  poimirlem26  38564  heibor1lem  38743  heiborlem3  38747  heiborlem10  38754  ablo4pnp  38814  crngm4  38937  lkrpssN  40220  pclvalN  40947  polvalN  40962  lclkrlem2x  42587  hgmaprnlem5N  42957  aks6d1c2p2  43169  unitscyglem2  43246  fsuppssindlem1  43619  onsupmaxb  44240  dvgrat  45295  radcnvrat  45297  sswfaxreg  45976  cncfiooicclem1  46902  fourierdlem101  47216  etransclem24  47267  ioorrnopn  47314  indprm  48713  isthincd2  50544