Theorem sylan2br 598

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  syl2anbr  602  pm2.61danel  3050  imainss  5997  funeu2  6384  imadif  6442  fnop  6465  ssimaex  6774  tfindsg2  7618  nn0suc  7651  xpexr2  7675  extmptsuppeq  7908  suppss  7914  suppssOLD  7915  suppss2  7920  frrlem14  8018  wfr3g  8031  smores3  8068  tfr3ALT  8116  tz7.48-2  8156  swoso  8402  entrfil  8840  isinf  8867  frfi  8894  dffi3  9025  marypha1lem  9027  ordtypelem7  9118  cnfcom2lem  9294  r1pw  9426  rankxplim3  9462  dfac5  9707  cofsmo  9848  axcclem  10036  zorn2lem7  10081  wloglei  11329  divval  11457  uzind3  12236  xrltnsym  12692  xaddf  12779  xrsupsslem  12862  xrinfmsslem  12863  0fz1  13097  hashunsng  13924  hashunsngx  13925  hashgt0elexb  13934  sumss  15253  fsumss  15254  fsumcvg3  15258  abscvgcvg  15346  isumshft  15366  geoisum1  15406  geoisum1c  15407  mertenslem2  15412  zprod  15462  prodss  15472  fprodss  15473  rpnnen2lem5  15742  gcdcllem3  16023  lcmgcd  16127  lcmdvds  16128  lcmfval  16141  lcmfcl  16148  dvdslcmf  16151  isprm2lem  16201  eulerthlem2  16298  ramcl2lem  16525  imasvscafn  16996  mreexexlem4d  17104  cycsubgcl  18567  galactghm  18750  odlem2  18885  gexlem2  18925  mulgmhm  19167  mulgghm  19168  gsumval3  19246  gsumpt  19301  dprdfeq0  19363  srglmhm  19504  srgrmhm  19505  ringlghm  19576  ringrghm  19577  sdrgacs  19799  cntzsdrg  19800  lssssr  19944  lbsind  20071  cnsubrg  20377  mplmonmul  20947  mplcoe1  20948  mplcoe5  20951  matplusgcell  21284  elcls  21924  neips  21964  opnnei  21971  ordtbaslem  22039  ptclsg  22466  qtopeu  22567  xmetpsmet  23200  comet  23365  metrest  23376  pcorevlem  23877  dyadmbl  24451  mbfeqalem1  24492  i1fadd  24546  itg1addlem2  24548  itg2uba  24595  itgss  24663  dvcnp  24770  quotval  25139  vieta1lem2  25158  aalioulem3  25181  ulmdvlem3  25248  dvradcnv  25267  abelthlem6  25282  abelthlem9  25286  abelth  25287  logtayllem  25501  logtayl  25502  cxpcl  25516  recxpcl  25517  cxpcn3lem  25587  leibpi  25779  musum  26027  dchrelbas3  26073  sumdchr2  26105  lgscllem  26139  lgsdir2  26165  dchrvmasumiflem2  26337  rpvmasum2  26347  padicabv  26465  padicabvf  26466  padicabvcxp  26467  1wlkdlem4  28177  nmooval  28798  hiidge0  29133  hommval  29771  hfmmval  29774  nmcfnlbi  30087  mdslmd1i  30364  mdslmd3i  30367  sumdmdlem2  30454  foresf1o  30523  disjdifprg  30587  cnvoprabOLD  30729  xdivval  30867  nsgqusf1olem2  31267  esumfsupre  31705  dya2iocnei  31915  eulerpartlemgc  31995  eulerpartlemb  32001  eulerpartlemgh  32011  ballotlemfc0  32125  ballotlemfcc  32126  subfacp1lem5  32813  subfacp1lem6  32814  cvmliftlem10  32923  elmrsubrn  33149  poxp2  33470  xpord3pred  33478  sexp3  33479  colinearperm1  34050  colinearperm5  34054  endofsegid  34073  segcon2  34093  seglecgr12im  34098  segletr  34102  colinbtwnle  34106  broutsideof2  34110  btwnoutside  34113  outsideoftr  34117  outsidele  34120  opnbnd  34200  ctbssinf  35263  matunitlindf  35461  poimirlem11  35474  poimirlem12  35475  poimirlem16  35479  poimirlem19  35482  poimirlem26  35489  heibor1lem  35653  heiborlem3  35657  heiborlem10  35664  ablo4pnp  35724  crngm4  35847  lkrpssN  36863  pclvalN  37590  polvalN  37605  lclkrlem2x  39230  hgmaprnlem5N  39600  fsuppssindlem1  39931  infdesc  40124  dvgrat  41544  radcnvrat  41546  cncfiooicclem1  43052  fourierdlem101  43366  etransclem24  43417  ioorrnopn  43464  isthincd2  45935