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  6122  funeu2  6528  imadif  6586  fnop  6611  ssimaex  6929  tfindsg2  7816  nn0suc  7848  xpexr2  7873  poxp2  8097  sexp3  8107  extmptsuppeq  8142  suppss  8148  suppss2  8154  frrlem14  8253  wfr3g  8273  smores3  8297  tfr3ALT  8345  tz7.48-2  8385  swoso  8682  entrfil  9123  domtrfil  9130  1sdom  9169  isinf  9179  frfi  9199  dffi3  9348  marypha1lem  9350  ordtypelem7  9443  cnfcom2lem  9624  r1pw  9771  rankxplim3  9807  dfac5  10053  cofsmo  10193  axcclem  10381  zorn2lem7  10426  wloglei  11683  divval  11812  uzind3  12600  xrltnsym  13065  xaddf  13153  xrsupsslem  13236  xrinfmsslem  13237  0fz1  13474  hashunsng  14329  hashunsngx  14330  hashgt0elexb  14339  sumss  15661  fsumss  15662  fsumcvg3  15666  abscvgcvg  15756  isumshft  15776  geoisum1  15816  geoisum1c  15817  mertenslem2  15822  zprod  15874  prodss  15884  fprodss  15885  rpnnen2lem5  16157  gcdcllem3  16442  lcmgcd  16548  lcmdvds  16549  lcmfval  16562  lcmfcl  16569  dvdslcmf  16572  isprm2lem  16622  eulerthlem2  16723  ramcl2lem  16951  imasvscafn  17472  mreexexlem4d  17584  issgrpd  18669  cycsubgcl  19152  galactghm  19350  odlem2  19485  gexlem2  19528  mulgmhm  19773  mulgghm  19774  gsumval3  19853  gsumpt  19908  dprdfeq0  19970  srglmhm  20173  srgrmhm  20174  ringlghm  20264  ringrghm  20265  sdrgacs  20751  cntzsdrg  20752  lssssr  20922  lbsind  21049  cnsubrg  21399  mplmonmul  22008  mplcoe1  22009  mplcoe5  22012  matplusgcell  22394  elcls  23034  neips  23074  opnnei  23081  ordtbaslem  23149  ptclsg  23576  qtopeu  23677  xmetpsmet  24309  comet  24474  metrest  24485  pcorevlem  24999  dyadmbl  25574  mbfeqalem1  25615  i1fadd  25669  itg1addlem2  25671  itg2uba  25717  itgss  25786  dvcnp  25893  quotval  26273  vieta1lem2  26292  aalioulem3  26315  ulmdvlem3  26384  dvradcnv  26403  abelthlem6  26419  abelthlem9  26423  abelth  26424  logtayllem  26641  logtayl  26642  cxpcl  26656  recxpcl  26657  cxpcn3lem  26730  leibpi  26925  musum  27174  dchrelbas3  27222  sumdchr2  27254  lgscllem  27288  lgsdir2  27314  dchrvmasumiflem2  27486  rpvmasum2  27496  padicabv  27614  padicabvf  27615  padicabvcxp  27616  mulsuniflem  28162  divsval  28202  1wlkdlem4  30233  nmooval  30857  hiidge0  31192  hommval  31830  hfmmval  31833  nmcfnlbi  32146  mdslmd1i  32423  mdslmd3i  32426  sumdmdlem2  32513  foresf1o  32597  disjdifprg  32668  xdivval  33017  nsgqusf1olem2  33513  ply1mulrtss  33681  psrmonmul  33733  esumfsupre  34255  dya2iocnei  34466  eulerpartlemgc  34546  eulerpartlemb  34552  eulerpartlemgh  34562  ballotlemfc0  34677  ballotlemfcc  34678  subfacp1lem5  35406  subfacp1lem6  35407  cvmliftlem10  35516  elmrsubrn  35742  colinearperm1  36284  colinearperm5  36288  endofsegid  36307  segcon2  36327  seglecgr12im  36332  segletr  36336  colinbtwnle  36340  broutsideof2  36344  btwnoutside  36347  outsideoftr  36351  outsidele  36354  opnbnd  36547  ctbssinf  37688  matunitlindf  37898  poimirlem11  37911  poimirlem12  37912  poimirlem16  37916  poimirlem19  37919  poimirlem26  37926  heibor1lem  38089  heiborlem3  38093  heiborlem10  38100  ablo4pnp  38160  crngm4  38283  lkrpssN  39568  pclvalN  40295  polvalN  40310  lclkrlem2x  41935  hgmaprnlem5N  42305  aks6d1c2p2  42518  unitscyglem2  42595  selvvvval  42972  fsuppssindlem1  42978  infdesc  43030  onsupmaxb  43625  dvgrat  44697  radcnvrat  44699  sswfaxreg  45372  cncfiooicclem1  46280  fourierdlem101  46594  etransclem24  46645  ioorrnopn  46692  isthincd2  49825