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  3060  imainss  6174  funeu2  6592  imadif  6650  fnop  6677  ssimaex  6994  tfindsg2  7883  nn0suc  7916  xpexr2  7941  poxp2  8168  sexp3  8178  extmptsuppeq  8213  suppss  8219  suppss2  8225  frrlem14  8324  wfr3g  8347  smores3  8393  tfr3ALT  8442  tz7.48-2  8482  swoso  8779  entrfil  9225  domtrfil  9232  1sdom  9284  isinf  9296  isinfOLD  9297  frfi  9321  dffi3  9471  marypha1lem  9473  ordtypelem7  9564  cnfcom2lem  9741  r1pw  9885  rankxplim3  9921  dfac5  10169  cofsmo  10309  axcclem  10497  zorn2lem7  10542  wloglei  11795  divval  11924  uzind3  12712  xrltnsym  13179  xaddf  13266  xrsupsslem  13349  xrinfmsslem  13350  0fz1  13584  hashunsng  14431  hashunsngx  14432  hashgt0elexb  14441  sumss  15760  fsumss  15761  fsumcvg3  15765  abscvgcvg  15855  isumshft  15875  geoisum1  15915  geoisum1c  15916  mertenslem2  15921  zprod  15973  prodss  15983  fprodss  15984  rpnnen2lem5  16254  gcdcllem3  16538  lcmgcd  16644  lcmdvds  16645  lcmfval  16658  lcmfcl  16665  dvdslcmf  16668  isprm2lem  16718  eulerthlem2  16819  ramcl2lem  17047  imasvscafn  17582  mreexexlem4d  17690  issgrpd  18743  cycsubgcl  19224  galactghm  19422  odlem2  19557  gexlem2  19600  mulgmhm  19845  mulgghm  19846  gsumval3  19925  gsumpt  19980  dprdfeq0  20042  srglmhm  20218  srgrmhm  20219  ringlghm  20309  ringrghm  20310  sdrgacs  20802  cntzsdrg  20803  lssssr  20952  lbsind  21079  cnsubrg  21445  mplmonmul  22054  mplcoe1  22055  mplcoe5  22058  matplusgcell  22439  elcls  23081  neips  23121  opnnei  23128  ordtbaslem  23196  ptclsg  23623  qtopeu  23724  xmetpsmet  24358  comet  24526  metrest  24537  pcorevlem  25059  dyadmbl  25635  mbfeqalem1  25676  i1fadd  25730  itg1addlem2  25732  itg2uba  25778  itgss  25847  dvcnp  25954  quotval  26334  vieta1lem2  26353  aalioulem3  26376  ulmdvlem3  26445  dvradcnv  26464  abelthlem6  26480  abelthlem9  26484  abelth  26485  logtayllem  26701  logtayl  26702  cxpcl  26716  recxpcl  26717  cxpcn3lem  26790  leibpi  26985  musum  27234  dchrelbas3  27282  sumdchr2  27314  lgscllem  27348  lgsdir2  27374  dchrvmasumiflem2  27546  rpvmasum2  27556  padicabv  27674  padicabvf  27675  padicabvcxp  27676  mulsuniflem  28175  divsval  28215  1wlkdlem4  30159  nmooval  30782  hiidge0  31117  hommval  31755  hfmmval  31758  nmcfnlbi  32071  mdslmd1i  32348  mdslmd3i  32351  sumdmdlem2  32438  foresf1o  32523  disjdifprg  32588  xdivval  32901  nsgqusf1olem2  33442  ply1mulrtss  33606  esumfsupre  34072  dya2iocnei  34284  eulerpartlemgc  34364  eulerpartlemb  34370  eulerpartlemgh  34380  ballotlemfc0  34495  ballotlemfcc  34496  subfacp1lem5  35189  subfacp1lem6  35190  cvmliftlem10  35299  elmrsubrn  35525  colinearperm1  36063  colinearperm5  36067  endofsegid  36086  segcon2  36106  seglecgr12im  36111  segletr  36115  colinbtwnle  36119  broutsideof2  36123  btwnoutside  36126  outsideoftr  36130  outsidele  36133  opnbnd  36326  ctbssinf  37407  matunitlindf  37625  poimirlem11  37638  poimirlem12  37639  poimirlem16  37643  poimirlem19  37646  poimirlem26  37653  heibor1lem  37816  heiborlem3  37820  heiborlem10  37827  ablo4pnp  37887  crngm4  38010  lkrpssN  39164  pclvalN  39892  polvalN  39907  lclkrlem2x  41532  hgmaprnlem5N  41902  aks6d1c2p2  42120  unitscyglem2  42197  selvvvval  42595  fsuppssindlem1  42601  infdesc  42653  onsupmaxb  43251  dvgrat  44331  radcnvrat  44333  sswfaxreg  45004  cncfiooicclem1  45908  fourierdlem101  46222  etransclem24  46273  ioorrnopn  46320  isthincd2  49086