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

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

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 397

This theorem is referenced by:  syl2anbr  599  pm2.61danel  3060  imainss  6153  funeu2  6574  imadif  6632  fnop  6658  ssimaex  6976  tfindsg2  7853  nn0suc  7888  xpexr2  7912  poxp2  8131  sexp3  8141  extmptsuppeq  8175  suppss  8181  suppssOLD  8182  suppss2  8187  frrlem14  8286  wfr3g  8309  smores3  8355  tfr3ALT  8404  tz7.48-2  8444  swoso  8738  entrfil  9190  domtrfil  9197  1sdom  9250  isinf  9262  isinfOLD  9263  frfi  9290  dffi3  9428  marypha1lem  9430  ordtypelem7  9521  cnfcom2lem  9698  r1pw  9842  rankxplim3  9878  dfac5  10125  cofsmo  10266  axcclem  10454  zorn2lem7  10499  wloglei  11748  divval  11876  uzind3  12658  xrltnsym  13118  xaddf  13205  xrsupsslem  13288  xrinfmsslem  13289  0fz1  13523  hashunsng  14354  hashunsngx  14355  hashgt0elexb  14364  sumss  15672  fsumss  15673  fsumcvg3  15677  abscvgcvg  15767  isumshft  15787  geoisum1  15827  geoisum1c  15828  mertenslem2  15833  zprod  15883  prodss  15893  fprodss  15894  rpnnen2lem5  16163  gcdcllem3  16444  lcmgcd  16546  lcmdvds  16547  lcmfval  16560  lcmfcl  16567  dvdslcmf  16570  isprm2lem  16620  eulerthlem2  16717  ramcl2lem  16944  imasvscafn  17485  mreexexlem4d  17593  issgrpd  18623  cycsubgcl  19085  galactghm  19274  odlem2  19409  gexlem2  19452  mulgmhm  19697  mulgghm  19698  gsumval3  19777  gsumpt  19832  dprdfeq0  19894  srglmhm  20046  srgrmhm  20047  ringlghm  20128  ringrghm  20129  sdrgacs  20421  cntzsdrg  20422  lssssr  20569  lbsind  20696  cnsubrg  21011  mplmonmul  21597  mplcoe1  21598  mplcoe5  21601  matplusgcell  21942  elcls  22584  neips  22624  opnnei  22631  ordtbaslem  22699  ptclsg  23126  qtopeu  23227  xmetpsmet  23861  comet  24029  metrest  24040  pcorevlem  24549  dyadmbl  25124  mbfeqalem1  25165  i1fadd  25219  itg1addlem2  25221  itg2uba  25268  itgss  25336  dvcnp  25443  quotval  25812  vieta1lem2  25831  aalioulem3  25854  ulmdvlem3  25921  dvradcnv  25940  abelthlem6  25955  abelthlem9  25959  abelth  25960  logtayllem  26174  logtayl  26175  cxpcl  26189  recxpcl  26190  cxpcn3lem  26262  leibpi  26454  musum  26702  dchrelbas3  26748  sumdchr2  26780  lgscllem  26814  lgsdir2  26840  dchrvmasumiflem2  27012  rpvmasum2  27022  padicabv  27140  padicabvf  27141  padicabvcxp  27142  mulsuniflem  27614  divsval  27647  1wlkdlem4  29431  nmooval  30054  hiidge0  30389  hommval  31027  hfmmval  31030  nmcfnlbi  31343  mdslmd1i  31620  mdslmd3i  31623  sumdmdlem2  31710  foresf1o  31780  disjdifprg  31844  cnvoprabOLD  31983  xdivval  32123  nsgqusf1olem2  32570  esumfsupre  33138  dya2iocnei  33350  eulerpartlemgc  33430  eulerpartlemb  33436  eulerpartlemgh  33446  ballotlemfc0  33560  ballotlemfcc  33561  subfacp1lem5  34244  subfacp1lem6  34245  cvmliftlem10  34354  elmrsubrn  34580  colinearperm1  35103  colinearperm5  35107  endofsegid  35126  segcon2  35146  seglecgr12im  35151  segletr  35155  colinbtwnle  35159  broutsideof2  35163  btwnoutside  35166  outsideoftr  35170  outsidele  35173  opnbnd  35296  ctbssinf  36373  matunitlindf  36572  poimirlem11  36585  poimirlem12  36586  poimirlem16  36590  poimirlem19  36593  poimirlem26  36600  heibor1lem  36763  heiborlem3  36767  heiborlem10  36774  ablo4pnp  36834  crngm4  36957  lkrpssN  38119  pclvalN  38847  polvalN  38862  lclkrlem2x  40487  hgmaprnlem5N  40857  aks6d1c2p2  41043  selvvvval  41239  fsuppssindlem1  41245  infdesc  41467  onsupmaxb  42070  dvgrat  43153  radcnvrat  43155  cncfiooicclem1  44688  fourierdlem101  45002  etransclem24  45053  ioorrnopn  45100  isthincd2  47736