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  3043  imainss  6115  funeu2  6526  imadif  6584  fnop  6609  ssimaex  6928  tfindsg2  7818  nn0suc  7850  xpexr2  7875  poxp2  8099  sexp3  8109  extmptsuppeq  8144  suppss  8150  suppss2  8156  frrlem14  8255  wfr3g  8275  smores3  8299  tfr3ALT  8347  tz7.48-2  8387  swoso  8682  entrfil  9126  domtrfil  9133  1sdom  9171  isinf  9183  isinfOLD  9184  frfi  9208  dffi3  9358  marypha1lem  9360  ordtypelem7  9453  cnfcom2lem  9630  r1pw  9774  rankxplim3  9810  dfac5  10058  cofsmo  10198  axcclem  10386  zorn2lem7  10431  wloglei  11686  divval  11815  uzind3  12604  xrltnsym  13073  xaddf  13160  xrsupsslem  13243  xrinfmsslem  13244  0fz1  13481  hashunsng  14333  hashunsngx  14334  hashgt0elexb  14343  sumss  15666  fsumss  15667  fsumcvg3  15671  abscvgcvg  15761  isumshft  15781  geoisum1  15821  geoisum1c  15822  mertenslem2  15827  zprod  15879  prodss  15889  fprodss  15890  rpnnen2lem5  16162  gcdcllem3  16447  lcmgcd  16553  lcmdvds  16554  lcmfval  16567  lcmfcl  16574  dvdslcmf  16577  isprm2lem  16627  eulerthlem2  16728  ramcl2lem  16956  imasvscafn  17476  mreexexlem4d  17588  issgrpd  18639  cycsubgcl  19120  galactghm  19318  odlem2  19453  gexlem2  19496  mulgmhm  19741  mulgghm  19742  gsumval3  19821  gsumpt  19876  dprdfeq0  19938  srglmhm  20141  srgrmhm  20142  ringlghm  20232  ringrghm  20233  sdrgacs  20721  cntzsdrg  20722  lssssr  20892  lbsind  21019  cnsubrg  21369  mplmonmul  21976  mplcoe1  21977  mplcoe5  21980  matplusgcell  22353  elcls  22993  neips  23033  opnnei  23040  ordtbaslem  23108  ptclsg  23535  qtopeu  23636  xmetpsmet  24269  comet  24434  metrest  24445  pcorevlem  24959  dyadmbl  25534  mbfeqalem1  25575  i1fadd  25629  itg1addlem2  25631  itg2uba  25677  itgss  25746  dvcnp  25853  quotval  26233  vieta1lem2  26252  aalioulem3  26275  ulmdvlem3  26344  dvradcnv  26363  abelthlem6  26379  abelthlem9  26383  abelth  26384  logtayllem  26601  logtayl  26602  cxpcl  26616  recxpcl  26617  cxpcn3lem  26690  leibpi  26885  musum  27134  dchrelbas3  27182  sumdchr2  27214  lgscllem  27248  lgsdir2  27274  dchrvmasumiflem2  27446  rpvmasum2  27456  padicabv  27574  padicabvf  27575  padicabvcxp  27576  mulsuniflem  28092  divsval  28132  1wlkdlem4  30119  nmooval  30742  hiidge0  31077  hommval  31715  hfmmval  31718  nmcfnlbi  32031  mdslmd1i  32308  mdslmd3i  32311  sumdmdlem2  32398  foresf1o  32483  disjdifprg  32554  xdivval  32889  nsgqusf1olem2  33378  ply1mulrtss  33543  esumfsupre  34054  dya2iocnei  34266  eulerpartlemgc  34346  eulerpartlemb  34352  eulerpartlemgh  34362  ballotlemfc0  34477  ballotlemfcc  34478  subfacp1lem5  35164  subfacp1lem6  35165  cvmliftlem10  35274  elmrsubrn  35500  colinearperm1  36043  colinearperm5  36047  endofsegid  36066  segcon2  36086  seglecgr12im  36091  segletr  36095  colinbtwnle  36099  broutsideof2  36103  btwnoutside  36106  outsideoftr  36110  outsidele  36113  opnbnd  36306  ctbssinf  37387  matunitlindf  37605  poimirlem11  37618  poimirlem12  37619  poimirlem16  37623  poimirlem19  37626  poimirlem26  37633  heibor1lem  37796  heiborlem3  37800  heiborlem10  37807  ablo4pnp  37867  crngm4  37990  lkrpssN  39149  pclvalN  39877  polvalN  39892  lclkrlem2x  41517  hgmaprnlem5N  41887  aks6d1c2p2  42100  unitscyglem2  42177  selvvvval  42566  fsuppssindlem1  42572  infdesc  42624  onsupmaxb  43221  dvgrat  44294  radcnvrat  44296  sswfaxreg  44970  cncfiooicclem1  45884  fourierdlem101  46198  etransclem24  46249  ioorrnopn  46296  isthincd2  49419