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  3049  imainss  6160  funeu2  6580  imadif  6638  fnop  6664  ssimaex  6982  tfindsg2  7867  nn0suc  7902  xpexr2  7927  poxp2  8148  sexp3  8158  extmptsuppeq  8193  suppss  8199  suppssOLD  8200  suppss2  8206  frrlem14  8305  wfr3g  8328  smores3  8374  tfr3ALT  8423  tz7.48-2  8463  swoso  8758  entrfil  9213  domtrfil  9220  1sdom  9273  isinf  9285  isinfOLD  9286  frfi  9313  dffi3  9456  marypha1lem  9458  ordtypelem7  9549  cnfcom2lem  9726  r1pw  9870  rankxplim3  9906  dfac5  10153  cofsmo  10294  axcclem  10482  zorn2lem7  10527  wloglei  11778  divval  11907  uzind3  12689  xrltnsym  13151  xaddf  13238  xrsupsslem  13321  xrinfmsslem  13322  0fz1  13556  hashunsng  14387  hashunsngx  14388  hashgt0elexb  14397  sumss  15706  fsumss  15707  fsumcvg3  15711  abscvgcvg  15801  isumshft  15821  geoisum1  15861  geoisum1c  15862  mertenslem2  15867  zprod  15917  prodss  15927  fprodss  15928  rpnnen2lem5  16198  gcdcllem3  16479  lcmgcd  16581  lcmdvds  16582  lcmfval  16595  lcmfcl  16602  dvdslcmf  16605  isprm2lem  16655  eulerthlem2  16754  ramcl2lem  16981  imasvscafn  17522  mreexexlem4d  17630  issgrpd  18693  cycsubgcl  19169  galactghm  19371  odlem2  19506  gexlem2  19549  mulgmhm  19794  mulgghm  19795  gsumval3  19874  gsumpt  19929  dprdfeq0  19991  srglmhm  20173  srgrmhm  20174  ringlghm  20260  ringrghm  20261  sdrgacs  20701  cntzsdrg  20702  lssssr  20850  lbsind  20977  cnsubrg  21377  mplmonmul  21996  mplcoe1  21997  mplcoe5  22000  matplusgcell  22379  elcls  23021  neips  23061  opnnei  23068  ordtbaslem  23136  ptclsg  23563  qtopeu  23664  xmetpsmet  24298  comet  24466  metrest  24477  pcorevlem  24997  dyadmbl  25573  mbfeqalem1  25614  i1fadd  25668  itg1addlem2  25670  itg2uba  25717  itgss  25785  dvcnp  25892  quotval  26272  vieta1lem2  26291  aalioulem3  26314  ulmdvlem3  26383  dvradcnv  26402  abelthlem6  26418  abelthlem9  26422  abelth  26423  logtayllem  26638  logtayl  26639  cxpcl  26653  recxpcl  26654  cxpcn3lem  26727  leibpi  26919  musum  27168  dchrelbas3  27216  sumdchr2  27248  lgscllem  27282  lgsdir2  27308  dchrvmasumiflem2  27480  rpvmasum2  27490  padicabv  27608  padicabvf  27609  padicabvcxp  27610  mulsuniflem  28099  divsval  28139  1wlkdlem4  30022  nmooval  30645  hiidge0  30980  hommval  31618  hfmmval  31621  nmcfnlbi  31934  mdslmd1i  32211  mdslmd3i  32214  sumdmdlem2  32301  foresf1o  32378  disjdifprg  32444  cnvoprabOLD  32584  xdivval  32727  nsgqusf1olem2  33226  ply1mulrtss  33390  esumfsupre  33821  dya2iocnei  34033  eulerpartlemgc  34113  eulerpartlemb  34119  eulerpartlemgh  34129  ballotlemfc0  34243  ballotlemfcc  34244  subfacp1lem5  34925  subfacp1lem6  34926  cvmliftlem10  35035  elmrsubrn  35261  colinearperm1  35789  colinearperm5  35793  endofsegid  35812  segcon2  35832  seglecgr12im  35837  segletr  35841  colinbtwnle  35845  broutsideof2  35849  btwnoutside  35852  outsideoftr  35856  outsidele  35859  opnbnd  35940  ctbssinf  37016  matunitlindf  37222  poimirlem11  37235  poimirlem12  37236  poimirlem16  37240  poimirlem19  37243  poimirlem26  37250  heibor1lem  37413  heiborlem3  37417  heiborlem10  37424  ablo4pnp  37484  crngm4  37607  lkrpssN  38765  pclvalN  39493  polvalN  39508  lclkrlem2x  41133  hgmaprnlem5N  41503  aks6d1c2p2  41722  selvvvval  41953  fsuppssindlem1  41959  infdesc  42202  onsupmaxb  42809  dvgrat  43891  radcnvrat  43893  cncfiooicclem1  45419  fourierdlem101  45733  etransclem24  45784  ioorrnopn  45831  isthincd2  48230