Theorem sylan2br 596

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  syl2anbr  600  pm2.61danel  3137  imainss  6006  funeu2  6376  imadif  6433  fnop  6455  ssimaex  6743  tfindsg2  7570  nn0suc  7600  xpexr2  7618  extmptsuppeq  7848  suppss  7854  suppss2  7858  wfr3g  7947  smores3  7984  tfr3ALT  8032  tz7.48-2  8072  swoso  8316  isinf  8725  frfi  8757  dffi3  8889  marypha1lem  8891  ordtypelem7  8982  cnfcom2lem  9158  r1pw  9268  rankxplim3  9304  dfac5  9548  cofsmo  9685  axcclem  9873  zorn2lem7  9918  wloglei  11166  divval  11294  uzind3  12070  xrltnsym  12524  xaddf  12611  xrsupsslem  12694  xrinfmsslem  12695  0fz1  12921  hashunsng  13747  hashunsngx  13748  hashgt0elexb  13757  sumss  15075  fsumss  15076  fsumcvg3  15080  abscvgcvg  15168  isumshft  15188  geoisum1  15229  geoisum1c  15230  mertenslem2  15235  zprod  15285  prodss  15295  fprodss  15296  rpnnen2lem5  15565  gcdcllem3  15844  lcmgcd  15945  lcmdvds  15946  lcmfval  15959  lcmfcl  15966  dvdslcmf  15969  isprm2lem  16019  eulerthlem2  16113  ramcl2lem  16339  imasvscafn  16804  mreexexlem4d  16912  cycsubgcl  18343  galactghm  18526  odlem2  18661  gexlem2  18701  mulgmhm  18942  mulgghm  18943  gsumval3  19021  gsumpt  19076  dprdfeq0  19138  srglmhm  19279  srgrmhm  19280  ringlghm  19348  ringrghm  19349  sdrgacs  19574  cntzsdrg  19575  lssssr  19719  lbsind  19846  mplmonmul  20239  mplcoe1  20240  mplcoe5  20243  cnsubrg  20599  matplusgcell  21036  elcls  21675  neips  21715  opnnei  21722  ordtbaslem  21790  ptclsg  22217  qtopeu  22318  xmetpsmet  22952  comet  23117  metrest  23128  pcorevlem  23624  dyadmbl  24195  mbfeqalem1  24236  i1fadd  24290  itg1addlem2  24292  itg2uba  24338  itgss  24406  dvcnp  24510  quotval  24875  vieta1lem2  24894  aalioulem3  24917  ulmdvlem3  24984  dvradcnv  25003  abelthlem6  25018  abelthlem9  25022  abelth  25023  logtayllem  25236  logtayl  25237  cxpcl  25251  recxpcl  25252  cxpcn3lem  25322  leibpi  25514  musum  25762  dchrelbas3  25808  sumdchr2  25840  lgscllem  25874  lgsdir2  25900  dchrvmasumiflem2  26072  rpvmasum2  26082  padicabv  26200  padicabvf  26201  padicabvcxp  26202  1wlkdlem4  27913  nmooval  28534  hiidge0  28869  hommval  29507  hfmmval  29510  nmcfnlbi  29823  mdslmd1i  30100  mdslmd3i  30103  sumdmdlem2  30190  foresf1o  30259  disjdifprg  30319  cnvoprabOLD  30450  xdivval  30590  esumfsupre  31325  dya2iocnei  31535  eulerpartlemgc  31615  eulerpartlemb  31621  eulerpartlemgh  31631  ballotlemfc0  31745  ballotlemfcc  31746  subfacp1lem5  32426  subfacp1lem6  32427  cvmliftlem10  32536  elmrsubrn  32762  frrlem14  33131  colinearperm1  33518  colinearperm5  33522  endofsegid  33541  segcon2  33561  seglecgr12im  33566  segletr  33570  colinbtwnle  33574  broutsideof2  33578  btwnoutside  33581  outsideoftr  33585  outsidele  33588  opnbnd  33668  ctbssinf  34681  matunitlindf  34884  poimirlem11  34897  poimirlem12  34898  poimirlem16  34902  poimirlem19  34905  poimirlem26  34912  heibor1lem  35081  heiborlem3  35085  heiborlem10  35092  ablo4pnp  35152  crngm4  35275  lkrpssN  36293  pclvalN  37020  polvalN  37035  lclkrlem2x  38660  hgmaprnlem5N  39030  dvgrat  40637  radcnvrat  40639  cncfiooicclem1  42168  fourierdlem101  42485  etransclem24  42536  ioorrnopn  42583