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  3080  imainss  6153  funeu2  6566  imadif  6624  fnop  6648  ssimaex  6970  tfindsg2  7864  nn0suc  7897  xpexr2  7922  poxp2  8145  sexp3  8155  extmptsuppeq  8190  suppss  8196  suppss2  8202  frrlem14  8302  wfr3g  8322  smores3  8346  tfr3ALT  8395  tz7.48-2  8435  swoso  8735  entrfil  9176  domtrfil  9183  1sdom  9222  isinf  9232  frfi  9252  dffi3  9398  marypha1lem  9400  ordtypelem7  9493  cnfcom2lem  9677  r1pw  9824  rankxplim3  9860  dfac5  10128  cofsmo  10268  axcclem  10456  zorn2lem7  10501  wloglei  11765  divval  11893  uzind3  12710  xrltnsym  13182  xaddf  13270  xrsupsslem  13353  xrinfmsslem  13354  0fz1  13592  hashunsng  14450  hashunsngx  14451  hashgt0elexb  14460  sumss  15802  fsumss  15803  fsumcvg3  15807  abscvgcvg  15898  isumshft  15920  geoisum1  15960  geoisum1c  15961  mertenslem2  15966  zprod  16018  prodss  16028  fprodss  16029  rpnnen2lem5  16300  gcdcllem3  16585  lcmgcd  16691  lcmdvds  16692  lcmfval  16705  lcmfcl  16712  dvdslcmf  16715  isprm2lem  16765  eulerthlem2  16867  ramcl2lem  17095  imasvscafn  17617  mreexexlem4d  17729  issgrpd  18824  cycsubgcl  19325  galactghm  19522  odlem2  19657  gexlem2  19700  mulgmhm  19945  mulgghm  19946  gsumval3  20025  gsumpt  20080  dprdfeq0  20142  srglmhm  20351  srgrmhm  20352  ringlghm  20445  ringrghm  20446  sdrgacs  20958  cntzsdrg  20959  lssssr  21129  lbsind  21255  cnsubrg  21631  mplmonmul  22241  mplcoe1  22242  mplcoe5  22245  selvvvval  22347  matplusgcell  22644  elcls  23284  neips  23324  opnnei  23331  ordtbaslem  23399  ptclsg  23827  qtopeu  23928  xmetpsmet  24560  comet  24725  metrest  24736  pcorevlem  25240  dyadmbl  25814  mbfeqalem1  25855  i1fadd  25909  itg1addlem2  25911  itg2uba  25957  itgss  26026  dvcnp  26133  quotval  26508  vieta1lem2  26527  aalioulem3  26552  ulmdvlem3  26620  dvradcnv  26639  abelthlem6  26654  abelthlem9  26658  abelth  26659  logtayllem  26879  logtayl  26880  cxpcl  26894  recxpcl  26895  cxpcn3lem  26967  leibpi  27162  musum  27410  dchrelbas3  27457  sumdchr2  27489  lgscllem  27523  lgsdir2  27549  dchrvmasumiflem2  27721  rpvmasum2  27731  padicabv  27849  padicabvf  27850  padicabvcxp  27851  mulsuniflem  28397  divsval  28437  1wlkdlem4  30562  nmooval  31190  hiidge0  31525  hommval  32163  hfmmval  32166  nmcfnlbi  32479  mdslmd1i  32756  mdslmd3i  32759  sumdmdlem2  32846  foresf1o  32925  disjdifprg  32995  xdivval  33312  nsgqusf1olem2  33791  ply1mulrtss  33940  psrmonmul  34008  esumfsupre  34529  dya2iocnei  34741  eulerpartlemgc  34821  eulerpartlemb  34827  eulerpartlemgh  34837  ballotlemfc0  34952  ballotlemfcc  34953  subfacp1lem5  35717  subfacp1lem6  35718  cvmliftlem10  35827  elmrsubrn  36053  colinearperm1  36595  colinearperm5  36599  endofsegid  36618  segcon2  36638  seglecgr12im  36643  segletr  36647  colinbtwnle  36651  broutsideof2  36655  btwnoutside  36658  outsideoftr  36662  outsidele  36665  opnbnd  36897  ctbssinf  38113  matunitlindf  38330  poimirlem11  38343  poimirlem12  38344  poimirlem16  38348  poimirlem19  38351  poimirlem26  38358  heibor1lem  38522  heiborlem3  38526  heiborlem10  38533  ablo4pnp  38593  crngm4  38716  lkrpssN  39999  pclvalN  40726  polvalN  40741  lclkrlem2x  42366  hgmaprnlem5N  42736  aks6d1c2p2  42948  unitscyglem2  43025  fsuppssindlem1  43400  infdesc  43452  onsupmaxb  44043  dvgrat  45099  radcnvrat  45101  sswfaxreg  45773  cncfiooicclem1  46684  fourierdlem101  46998  etransclem24  47049  ioorrnopn  47096  indprm  48458  isthincd2  50291