Theorem sylan2br 593

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

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

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 395

This theorem is referenced by:  syl2anbr  597  pm2.61danel  3057  imainss  6163  funeu2  6584  imadif  6642  fnop  6668  ssimaex  6988  tfindsg2  7874  nn0suc  7909  xpexr2  7935  poxp2  8156  sexp3  8166  extmptsuppeq  8201  suppss  8207  suppssOLD  8208  suppss2  8214  frrlem14  8313  wfr3g  8336  smores3  8382  tfr3ALT  8431  tz7.48-2  8471  swoso  8766  entrfil  9221  domtrfil  9228  1sdom  9281  isinf  9293  isinfOLD  9294  frfi  9321  dffi3  9464  marypha1lem  9466  ordtypelem7  9557  cnfcom2lem  9734  r1pw  9878  rankxplim3  9914  dfac5  10161  cofsmo  10302  axcclem  10490  zorn2lem7  10535  wloglei  11786  divval  11914  uzind3  12696  xrltnsym  13158  xaddf  13245  xrsupsslem  13328  xrinfmsslem  13329  0fz1  13563  hashunsng  14393  hashunsngx  14394  hashgt0elexb  14403  sumss  15712  fsumss  15713  fsumcvg3  15717  abscvgcvg  15807  isumshft  15827  geoisum1  15867  geoisum1c  15868  mertenslem2  15873  zprod  15923  prodss  15933  fprodss  15934  rpnnen2lem5  16204  gcdcllem3  16485  lcmgcd  16587  lcmdvds  16588  lcmfval  16601  lcmfcl  16608  dvdslcmf  16611  isprm2lem  16661  eulerthlem2  16760  ramcl2lem  16987  imasvscafn  17528  mreexexlem4d  17636  issgrpd  18699  cycsubgcl  19175  galactghm  19373  odlem2  19508  gexlem2  19551  mulgmhm  19796  mulgghm  19797  gsumval3  19876  gsumpt  19931  dprdfeq0  19993  srglmhm  20175  srgrmhm  20176  ringlghm  20262  ringrghm  20263  sdrgacs  20703  cntzsdrg  20704  lssssr  20852  lbsind  20979  cnsubrg  21374  mplmonmul  21991  mplcoe1  21992  mplcoe5  21995  matplusgcell  22363  elcls  23005  neips  23045  opnnei  23052  ordtbaslem  23120  ptclsg  23547  qtopeu  23648  xmetpsmet  24282  comet  24450  metrest  24461  pcorevlem  24981  dyadmbl  25557  mbfeqalem1  25598  i1fadd  25652  itg1addlem2  25654  itg2uba  25701  itgss  25769  dvcnp  25876  quotval  26255  vieta1lem2  26274  aalioulem3  26297  ulmdvlem3  26366  dvradcnv  26385  abelthlem6  26401  abelthlem9  26405  abelth  26406  logtayllem  26621  logtayl  26622  cxpcl  26636  recxpcl  26637  cxpcn3lem  26710  leibpi  26902  musum  27151  dchrelbas3  27199  sumdchr2  27231  lgscllem  27265  lgsdir2  27291  dchrvmasumiflem2  27463  rpvmasum2  27473  padicabv  27591  padicabvf  27592  padicabvcxp  27593  mulsuniflem  28077  divsval  28117  1wlkdlem4  29978  nmooval  30601  hiidge0  30936  hommval  31574  hfmmval  31577  nmcfnlbi  31890  mdslmd1i  32167  mdslmd3i  32170  sumdmdlem2  32257  foresf1o  32329  disjdifprg  32394  cnvoprabOLD  32531  xdivval  32671  nsgqusf1olem2  33157  esumfsupre  33731  dya2iocnei  33943  eulerpartlemgc  34023  eulerpartlemb  34029  eulerpartlemgh  34039  ballotlemfc0  34153  ballotlemfcc  34154  subfacp1lem5  34835  subfacp1lem6  34836  cvmliftlem10  34945  elmrsubrn  35171  colinearperm1  35699  colinearperm5  35703  endofsegid  35722  segcon2  35742  seglecgr12im  35747  segletr  35751  colinbtwnle  35755  broutsideof2  35759  btwnoutside  35762  outsideoftr  35766  outsidele  35769  opnbnd  35850  ctbssinf  36926  matunitlindf  37132  poimirlem11  37145  poimirlem12  37146  poimirlem16  37150  poimirlem19  37153  poimirlem26  37160  heibor1lem  37323  heiborlem3  37327  heiborlem10  37334  ablo4pnp  37394  crngm4  37517  lkrpssN  38675  pclvalN  39403  polvalN  39418  lclkrlem2x  41043  hgmaprnlem5N  41413  aks6d1c2p2  41630  selvvvval  41867  fsuppssindlem1  41873  infdesc  42116  onsupmaxb  42716  dvgrat  43798  radcnvrat  43800  cncfiooicclem1  45328  fourierdlem101  45642  etransclem24  45693  ioorrnopn  45740  isthincd2  48140