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 228	. 2 ⊢ (𝜑 → 𝜒)
3		sylan2br.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan2 594	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  600  pm2.61danel  3051  imainss  6113  funeu2  6519  imadif  6577  fnop  6602  ssimaex  6920  tfindsg2  7806  nn0suc  7838  xpexr2  7863  poxp2  8087  sexp3  8097  extmptsuppeq  8132  suppss  8138  suppss2  8144  frrlem14  8243  wfr3g  8263  smores3  8287  tfr3ALT  8335  tz7.48-2  8375  swoso  8672  entrfil  9113  domtrfil  9120  1sdom  9159  isinf  9169  frfi  9189  dffi3  9338  marypha1lem  9340  ordtypelem7  9433  cnfcom2lem  9614  r1pw  9761  rankxplim3  9797  dfac5  10043  cofsmo  10183  axcclem  10371  zorn2lem7  10416  wloglei  11673  divval  11802  uzind3  12590  xrltnsym  13055  xaddf  13143  xrsupsslem  13226  xrinfmsslem  13227  0fz1  13464  hashunsng  14319  hashunsngx  14320  hashgt0elexb  14329  sumss  15651  fsumss  15652  fsumcvg3  15656  abscvgcvg  15746  isumshft  15766  geoisum1  15806  geoisum1c  15807  mertenslem2  15812  zprod  15864  prodss  15874  fprodss  15875  rpnnen2lem5  16147  gcdcllem3  16432  lcmgcd  16538  lcmdvds  16539  lcmfval  16552  lcmfcl  16559  dvdslcmf  16562  isprm2lem  16612  eulerthlem2  16713  ramcl2lem  16941  imasvscafn  17462  mreexexlem4d  17574  issgrpd  18659  cycsubgcl  19139  galactghm  19337  odlem2  19472  gexlem2  19515  mulgmhm  19760  mulgghm  19761  gsumval3  19840  gsumpt  19895  dprdfeq0  19957  srglmhm  20160  srgrmhm  20161  ringlghm  20251  ringrghm  20252  sdrgacs  20738  cntzsdrg  20739  lssssr  20909  lbsind  21036  cnsubrg  21386  mplmonmul  21995  mplcoe1  21996  mplcoe5  21999  matplusgcell  22381  elcls  23021  neips  23061  opnnei  23068  ordtbaslem  23136  ptclsg  23563  qtopeu  23664  xmetpsmet  24296  comet  24461  metrest  24472  pcorevlem  24986  dyadmbl  25561  mbfeqalem1  25602  i1fadd  25656  itg1addlem2  25658  itg2uba  25704  itgss  25773  dvcnp  25880  quotval  26260  vieta1lem2  26279  aalioulem3  26302  ulmdvlem3  26371  dvradcnv  26390  abelthlem6  26406  abelthlem9  26410  abelth  26411  logtayllem  26628  logtayl  26629  cxpcl  26643  recxpcl  26644  cxpcn3lem  26717  leibpi  26912  musum  27161  dchrelbas3  27209  sumdchr2  27241  lgscllem  27275  lgsdir2  27301  dchrvmasumiflem2  27473  rpvmasum2  27483  padicabv  27601  padicabvf  27602  padicabvcxp  27603  mulsuniflem  28149  divsval  28189  1wlkdlem4  30219  nmooval  30842  hiidge0  31177  hommval  31815  hfmmval  31818  nmcfnlbi  32131  mdslmd1i  32408  mdslmd3i  32411  sumdmdlem2  32498  foresf1o  32582  disjdifprg  32653  xdivval  33002  nsgqusf1olem2  33497  ply1mulrtss  33665  esumfsupre  34230  dya2iocnei  34441  eulerpartlemgc  34521  eulerpartlemb  34527  eulerpartlemgh  34537  ballotlemfc0  34652  ballotlemfcc  34653  subfacp1lem5  35380  subfacp1lem6  35381  cvmliftlem10  35490  elmrsubrn  35716  colinearperm1  36258  colinearperm5  36262  endofsegid  36281  segcon2  36301  seglecgr12im  36306  segletr  36310  colinbtwnle  36314  broutsideof2  36318  btwnoutside  36321  outsideoftr  36325  outsidele  36328  opnbnd  36521  ctbssinf  37613  matunitlindf  37821  poimirlem11  37834  poimirlem12  37835  poimirlem16  37839  poimirlem19  37842  poimirlem26  37849  heibor1lem  38012  heiborlem3  38016  heiborlem10  38023  ablo4pnp  38083  crngm4  38206  lkrpssN  39491  pclvalN  40218  polvalN  40233  lclkrlem2x  41858  hgmaprnlem5N  42228  aks6d1c2p2  42441  unitscyglem2  42518  selvvvval  42895  fsuppssindlem1  42901  infdesc  42953  onsupmaxb  43548  dvgrat  44620  radcnvrat  44622  sswfaxreg  45295  cncfiooicclem1  46204  fourierdlem101  46518  etransclem24  46569  ioorrnopn  46616  isthincd2  49749