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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  syl2anbr  600  pm2.61danel  3061  imainss  6151  funeu2  6572  imadif  6630  fnop  6656  ssimaex  6974  tfindsg2  7848  nn0suc  7883  xpexr2  7907  poxp2  8126  sexp3  8136  extmptsuppeq  8170  suppss  8176  suppssOLD  8177  suppss2  8182  frrlem14  8281  wfr3g  8304  smores3  8350  tfr3ALT  8399  tz7.48-2  8439  swoso  8733  entrfil  9185  domtrfil  9192  1sdom  9245  isinf  9257  isinfOLD  9258  frfi  9285  dffi3  9423  marypha1lem  9425  ordtypelem7  9516  cnfcom2lem  9693  r1pw  9837  rankxplim3  9873  dfac5  10120  cofsmo  10261  axcclem  10449  zorn2lem7  10494  wloglei  11743  divval  11871  uzind3  12653  xrltnsym  13113  xaddf  13200  xrsupsslem  13283  xrinfmsslem  13284  0fz1  13518  hashunsng  14349  hashunsngx  14350  hashgt0elexb  14359  sumss  15667  fsumss  15668  fsumcvg3  15672  abscvgcvg  15762  isumshft  15782  geoisum1  15822  geoisum1c  15823  mertenslem2  15828  zprod  15878  prodss  15888  fprodss  15889  rpnnen2lem5  16158  gcdcllem3  16439  lcmgcd  16541  lcmdvds  16542  lcmfval  16555  lcmfcl  16562  dvdslcmf  16565  isprm2lem  16615  eulerthlem2  16712  ramcl2lem  16939  imasvscafn  17480  mreexexlem4d  17588  issgrpd  18618  cycsubgcl  19078  galactghm  19267  odlem2  19402  gexlem2  19445  mulgmhm  19690  mulgghm  19691  gsumval3  19770  gsumpt  19825  dprdfeq0  19887  srglmhm  20038  srgrmhm  20039  ringlghm  20118  ringrghm  20119  sdrgacs  20410  cntzsdrg  20411  lssssr  20557  lbsind  20684  cnsubrg  20998  mplmonmul  21583  mplcoe1  21584  mplcoe5  21587  matplusgcell  21927  elcls  22569  neips  22609  opnnei  22616  ordtbaslem  22684  ptclsg  23111  qtopeu  23212  xmetpsmet  23846  comet  24014  metrest  24025  pcorevlem  24534  dyadmbl  25109  mbfeqalem1  25150  i1fadd  25204  itg1addlem2  25206  itg2uba  25253  itgss  25321  dvcnp  25428  quotval  25797  vieta1lem2  25816  aalioulem3  25839  ulmdvlem3  25906  dvradcnv  25925  abelthlem6  25940  abelthlem9  25944  abelth  25945  logtayllem  26159  logtayl  26160  cxpcl  26174  recxpcl  26175  cxpcn3lem  26245  leibpi  26437  musum  26685  dchrelbas3  26731  sumdchr2  26763  lgscllem  26797  lgsdir2  26823  dchrvmasumiflem2  26995  rpvmasum2  27005  padicabv  27123  padicabvf  27124  padicabvcxp  27125  mulsuniflem  27594  divsval  27627  1wlkdlem4  29383  nmooval  30004  hiidge0  30339  hommval  30977  hfmmval  30980  nmcfnlbi  31293  mdslmd1i  31570  mdslmd3i  31573  sumdmdlem2  31660  foresf1o  31730  disjdifprg  31794  cnvoprabOLD  31933  xdivval  32073  nsgqusf1olem2  32514  esumfsupre  33058  dya2iocnei  33270  eulerpartlemgc  33350  eulerpartlemb  33356  eulerpartlemgh  33366  ballotlemfc0  33480  ballotlemfcc  33481  subfacp1lem5  34164  subfacp1lem6  34165  cvmliftlem10  34274  elmrsubrn  34500  colinearperm1  35023  colinearperm5  35027  endofsegid  35046  segcon2  35066  seglecgr12im  35071  segletr  35075  colinbtwnle  35079  broutsideof2  35083  btwnoutside  35086  outsideoftr  35090  outsidele  35093  opnbnd  35199  ctbssinf  36276  matunitlindf  36475  poimirlem11  36488  poimirlem12  36489  poimirlem16  36493  poimirlem19  36496  poimirlem26  36503  heibor1lem  36666  heiborlem3  36670  heiborlem10  36677  ablo4pnp  36737  crngm4  36860  lkrpssN  38022  pclvalN  38750  polvalN  38765  lclkrlem2x  40390  hgmaprnlem5N  40760  aks6d1c2p2  40946  selvvvval  41155  fsuppssindlem1  41161  infdesc  41382  onsupmaxb  41974  dvgrat  43057  radcnvrat  43059  cncfiooicclem1  44596  fourierdlem101  44910  etransclem24  44961  ioorrnopn  45008  isthincd2  47612