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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  syl2anbr  599  pm2.61danel  3064  imainss  6062  funeu2  6467  imadif  6525  fnop  6551  ssimaex  6862  tfindsg2  7717  nn0suc  7751  xpexr2  7775  extmptsuppeq  8013  suppss  8019  suppssOLD  8020  suppss2  8025  frrlem14  8124  wfr3g  8147  smores3  8193  tfr3ALT  8242  tz7.48-2  8282  swoso  8540  entrfil  8980  domtrfil  8987  isinf  9045  frfi  9068  dffi3  9199  marypha1lem  9201  ordtypelem7  9292  cnfcom2lem  9468  r1pw  9612  rankxplim3  9648  dfac5  9893  cofsmo  10034  axcclem  10222  zorn2lem7  10267  wloglei  11516  divval  11644  uzind3  12423  xrltnsym  12880  xaddf  12967  xrsupsslem  13050  xrinfmsslem  13051  0fz1  13285  hashunsng  14116  hashunsngx  14117  hashgt0elexb  14126  sumss  15445  fsumss  15446  fsumcvg3  15450  abscvgcvg  15540  isumshft  15560  geoisum1  15600  geoisum1c  15601  mertenslem2  15606  zprod  15656  prodss  15666  fprodss  15667  rpnnen2lem5  15936  gcdcllem3  16217  lcmgcd  16321  lcmdvds  16322  lcmfval  16335  lcmfcl  16342  dvdslcmf  16345  isprm2lem  16395  eulerthlem2  16492  ramcl2lem  16719  imasvscafn  17257  mreexexlem4d  17365  cycsubgcl  18834  galactghm  19021  odlem2  19156  gexlem2  19196  mulgmhm  19438  mulgghm  19439  gsumval3  19517  gsumpt  19572  dprdfeq0  19634  srglmhm  19780  srgrmhm  19781  ringlghm  19852  ringrghm  19853  sdrgacs  20078  cntzsdrg  20079  lssssr  20224  lbsind  20351  cnsubrg  20667  mplmonmul  21246  mplcoe1  21247  mplcoe5  21250  matplusgcell  21591  elcls  22233  neips  22273  opnnei  22280  ordtbaslem  22348  ptclsg  22775  qtopeu  22876  xmetpsmet  23510  comet  23678  metrest  23689  pcorevlem  24198  dyadmbl  24773  mbfeqalem1  24814  i1fadd  24868  itg1addlem2  24870  itg2uba  24917  itgss  24985  dvcnp  25092  quotval  25461  vieta1lem2  25480  aalioulem3  25503  ulmdvlem3  25570  dvradcnv  25589  abelthlem6  25604  abelthlem9  25608  abelth  25609  logtayllem  25823  logtayl  25824  cxpcl  25838  recxpcl  25839  cxpcn3lem  25909  leibpi  26101  musum  26349  dchrelbas3  26395  sumdchr2  26427  lgscllem  26461  lgsdir2  26487  dchrvmasumiflem2  26659  rpvmasum2  26669  padicabv  26787  padicabvf  26788  padicabvcxp  26789  1wlkdlem4  28513  nmooval  29134  hiidge0  29469  hommval  30107  hfmmval  30110  nmcfnlbi  30423  mdslmd1i  30700  mdslmd3i  30703  sumdmdlem2  30790  foresf1o  30859  disjdifprg  30923  cnvoprabOLD  31064  xdivval  31202  nsgqusf1olem2  31608  esumfsupre  32048  dya2iocnei  32258  eulerpartlemgc  32338  eulerpartlemb  32344  eulerpartlemgh  32354  ballotlemfc0  32468  ballotlemfcc  32469  subfacp1lem5  33155  subfacp1lem6  33156  cvmliftlem10  33265  elmrsubrn  33491  poxp2  33799  xpord3pred  33807  sexp3  33808  colinearperm1  34373  colinearperm5  34377  endofsegid  34396  segcon2  34416  seglecgr12im  34421  segletr  34425  colinbtwnle  34429  broutsideof2  34433  btwnoutside  34436  outsideoftr  34440  outsidele  34443  opnbnd  34523  ctbssinf  35586  matunitlindf  35784  poimirlem11  35797  poimirlem12  35798  poimirlem16  35802  poimirlem19  35805  poimirlem26  35812  heibor1lem  35976  heiborlem3  35980  heiborlem10  35987  ablo4pnp  36047  crngm4  36170  lkrpssN  37184  pclvalN  37911  polvalN  37926  lclkrlem2x  39551  hgmaprnlem5N  39921  fsuppssindlem1  40287  infdesc  40487  dvgrat  41937  radcnvrat  41939  cncfiooicclem1  43441  fourierdlem101  43755  etransclem24  43806  ioorrnopn  43853  isthincd2  46330