Theorem sylan2br 595

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 593	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  599  pm2.61danel  3046  imainss  6101  funeu2  6507  imadif  6565  fnop  6590  ssimaex  6907  tfindsg2  7792  nn0suc  7824  xpexr2  7849  poxp2  8073  sexp3  8083  extmptsuppeq  8118  suppss  8124  suppss2  8130  frrlem14  8229  wfr3g  8249  smores3  8273  tfr3ALT  8321  tz7.48-2  8361  swoso  8656  entrfil  9094  domtrfil  9101  1sdom  9139  isinf  9149  frfi  9169  dffi3  9315  marypha1lem  9317  ordtypelem7  9410  cnfcom2lem  9591  r1pw  9738  rankxplim3  9774  dfac5  10020  cofsmo  10160  axcclem  10348  zorn2lem7  10393  wloglei  11649  divval  11778  uzind3  12567  xrltnsym  13036  xaddf  13123  xrsupsslem  13206  xrinfmsslem  13207  0fz1  13444  hashunsng  14299  hashunsngx  14300  hashgt0elexb  14309  sumss  15631  fsumss  15632  fsumcvg3  15636  abscvgcvg  15726  isumshft  15746  geoisum1  15786  geoisum1c  15787  mertenslem2  15792  zprod  15844  prodss  15854  fprodss  15855  rpnnen2lem5  16127  gcdcllem3  16412  lcmgcd  16518  lcmdvds  16519  lcmfval  16532  lcmfcl  16539  dvdslcmf  16542  isprm2lem  16592  eulerthlem2  16693  ramcl2lem  16921  imasvscafn  17441  mreexexlem4d  17553  issgrpd  18638  cycsubgcl  19118  galactghm  19316  odlem2  19451  gexlem2  19494  mulgmhm  19739  mulgghm  19740  gsumval3  19819  gsumpt  19874  dprdfeq0  19936  srglmhm  20139  srgrmhm  20140  ringlghm  20230  ringrghm  20231  sdrgacs  20716  cntzsdrg  20717  lssssr  20887  lbsind  21014  cnsubrg  21364  mplmonmul  21971  mplcoe1  21972  mplcoe5  21975  matplusgcell  22348  elcls  22988  neips  23028  opnnei  23035  ordtbaslem  23103  ptclsg  23530  qtopeu  23631  xmetpsmet  24263  comet  24428  metrest  24439  pcorevlem  24953  dyadmbl  25528  mbfeqalem1  25569  i1fadd  25623  itg1addlem2  25625  itg2uba  25671  itgss  25740  dvcnp  25847  quotval  26227  vieta1lem2  26246  aalioulem3  26269  ulmdvlem3  26338  dvradcnv  26357  abelthlem6  26373  abelthlem9  26377  abelth  26378  logtayllem  26595  logtayl  26596  cxpcl  26610  recxpcl  26611  cxpcn3lem  26684  leibpi  26879  musum  27128  dchrelbas3  27176  sumdchr2  27208  lgscllem  27242  lgsdir2  27268  dchrvmasumiflem2  27440  rpvmasum2  27450  padicabv  27568  padicabvf  27569  padicabvcxp  27570  mulsuniflem  28088  divsval  28128  1wlkdlem4  30120  nmooval  30743  hiidge0  31078  hommval  31716  hfmmval  31719  nmcfnlbi  32032  mdslmd1i  32309  mdslmd3i  32312  sumdmdlem2  32399  foresf1o  32484  disjdifprg  32555  xdivval  32899  nsgqusf1olem2  33379  ply1mulrtss  33545  esumfsupre  34084  dya2iocnei  34295  eulerpartlemgc  34375  eulerpartlemb  34381  eulerpartlemgh  34391  ballotlemfc0  34506  ballotlemfcc  34507  subfacp1lem5  35228  subfacp1lem6  35229  cvmliftlem10  35338  elmrsubrn  35564  colinearperm1  36106  colinearperm5  36110  endofsegid  36129  segcon2  36149  seglecgr12im  36154  segletr  36158  colinbtwnle  36162  broutsideof2  36166  btwnoutside  36169  outsideoftr  36173  outsidele  36176  opnbnd  36369  ctbssinf  37450  matunitlindf  37657  poimirlem11  37670  poimirlem12  37671  poimirlem16  37675  poimirlem19  37678  poimirlem26  37685  heibor1lem  37848  heiborlem3  37852  heiborlem10  37859  ablo4pnp  37919  crngm4  38042  lkrpssN  39261  pclvalN  39988  polvalN  40003  lclkrlem2x  41628  hgmaprnlem5N  41998  aks6d1c2p2  42211  unitscyglem2  42288  selvvvval  42677  fsuppssindlem1  42683  infdesc  42735  onsupmaxb  43331  dvgrat  44404  radcnvrat  44406  sswfaxreg  45079  cncfiooicclem1  45990  fourierdlem101  46304  etransclem24  46355  ioorrnopn  46402  isthincd2  49537