Theorem sylan2br 594

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  syl2anbr  598  pm2.61danel  3066  imainss  6185  funeu2  6604  imadif  6662  fnop  6688  ssimaex  7007  tfindsg2  7899  nn0suc  7934  xpexr2  7959  poxp2  8184  sexp3  8194  extmptsuppeq  8229  suppss  8235  suppss2  8241  frrlem14  8340  wfr3g  8363  smores3  8409  tfr3ALT  8458  tz7.48-2  8498  swoso  8797  entrfil  9251  domtrfil  9258  1sdom  9311  isinf  9323  isinfOLD  9324  frfi  9349  dffi3  9500  marypha1lem  9502  ordtypelem7  9593  cnfcom2lem  9770  r1pw  9914  rankxplim3  9950  dfac5  10198  cofsmo  10338  axcclem  10526  zorn2lem7  10571  wloglei  11822  divval  11951  uzind3  12737  xrltnsym  13199  xaddf  13286  xrsupsslem  13369  xrinfmsslem  13370  0fz1  13604  hashunsng  14441  hashunsngx  14442  hashgt0elexb  14451  sumss  15772  fsumss  15773  fsumcvg3  15777  abscvgcvg  15867  isumshft  15887  geoisum1  15927  geoisum1c  15928  mertenslem2  15933  zprod  15985  prodss  15995  fprodss  15996  rpnnen2lem5  16266  gcdcllem3  16547  lcmgcd  16654  lcmdvds  16655  lcmfval  16668  lcmfcl  16675  dvdslcmf  16678  isprm2lem  16728  eulerthlem2  16829  ramcl2lem  17056  imasvscafn  17597  mreexexlem4d  17705  issgrpd  18768  cycsubgcl  19246  galactghm  19446  odlem2  19581  gexlem2  19624  mulgmhm  19869  mulgghm  19870  gsumval3  19949  gsumpt  20004  dprdfeq0  20066  srglmhm  20248  srgrmhm  20249  ringlghm  20335  ringrghm  20336  sdrgacs  20824  cntzsdrg  20825  lssssr  20975  lbsind  21102  cnsubrg  21468  mplmonmul  22077  mplcoe1  22078  mplcoe5  22081  matplusgcell  22460  elcls  23102  neips  23142  opnnei  23149  ordtbaslem  23217  ptclsg  23644  qtopeu  23745  xmetpsmet  24379  comet  24547  metrest  24558  pcorevlem  25078  dyadmbl  25654  mbfeqalem1  25695  i1fadd  25749  itg1addlem2  25751  itg2uba  25798  itgss  25867  dvcnp  25974  quotval  26352  vieta1lem2  26371  aalioulem3  26394  ulmdvlem3  26463  dvradcnv  26482  abelthlem6  26498  abelthlem9  26502  abelth  26503  logtayllem  26719  logtayl  26720  cxpcl  26734  recxpcl  26735  cxpcn3lem  26808  leibpi  27003  musum  27252  dchrelbas3  27300  sumdchr2  27332  lgscllem  27366  lgsdir2  27392  dchrvmasumiflem2  27564  rpvmasum2  27574  padicabv  27692  padicabvf  27693  padicabvcxp  27694  mulsuniflem  28193  divsval  28233  1wlkdlem4  30172  nmooval  30795  hiidge0  31130  hommval  31768  hfmmval  31771  nmcfnlbi  32084  mdslmd1i  32361  mdslmd3i  32364  sumdmdlem2  32451  foresf1o  32532  disjdifprg  32597  cnvoprabOLD  32734  xdivval  32883  nsgqusf1olem2  33407  ply1mulrtss  33571  esumfsupre  34035  dya2iocnei  34247  eulerpartlemgc  34327  eulerpartlemb  34333  eulerpartlemgh  34343  ballotlemfc0  34457  ballotlemfcc  34458  subfacp1lem5  35152  subfacp1lem6  35153  cvmliftlem10  35262  elmrsubrn  35488  colinearperm1  36026  colinearperm5  36030  endofsegid  36049  segcon2  36069  seglecgr12im  36074  segletr  36078  colinbtwnle  36082  broutsideof2  36086  btwnoutside  36089  outsideoftr  36093  outsidele  36096  opnbnd  36291  ctbssinf  37372  matunitlindf  37578  poimirlem11  37591  poimirlem12  37592  poimirlem16  37596  poimirlem19  37599  poimirlem26  37606  heibor1lem  37769  heiborlem3  37773  heiborlem10  37780  ablo4pnp  37840  crngm4  37963  lkrpssN  39119  pclvalN  39847  polvalN  39862  lclkrlem2x  41487  hgmaprnlem5N  41857  aks6d1c2p2  42076  unitscyglem2  42153  selvvvval  42540  fsuppssindlem1  42546  infdesc  42598  onsupmaxb  43200  dvgrat  44281  radcnvrat  44283  cncfiooicclem1  45814  fourierdlem101  46128  etransclem24  46179  ioorrnopn  46226  isthincd2  48705