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  6127  funeu2  6542  imadif  6600  fnop  6627  ssimaex  6946  tfindsg2  7838  nn0suc  7870  xpexr2  7895  poxp2  8122  sexp3  8132  extmptsuppeq  8167  suppss  8173  suppss2  8179  frrlem14  8278  wfr3g  8298  smores3  8322  tfr3ALT  8370  tz7.48-2  8410  swoso  8705  entrfil  9149  domtrfil  9156  1sdom  9195  isinf  9207  isinfOLD  9208  frfi  9232  dffi3  9382  marypha1lem  9384  ordtypelem7  9477  cnfcom2lem  9654  r1pw  9798  rankxplim3  9834  dfac5  10082  cofsmo  10222  axcclem  10410  zorn2lem7  10455  wloglei  11710  divval  11839  uzind3  12628  xrltnsym  13097  xaddf  13184  xrsupsslem  13267  xrinfmsslem  13268  0fz1  13505  hashunsng  14357  hashunsngx  14358  hashgt0elexb  14367  sumss  15690  fsumss  15691  fsumcvg3  15695  abscvgcvg  15785  isumshft  15805  geoisum1  15845  geoisum1c  15846  mertenslem2  15851  zprod  15903  prodss  15913  fprodss  15914  rpnnen2lem5  16186  gcdcllem3  16471  lcmgcd  16577  lcmdvds  16578  lcmfval  16591  lcmfcl  16598  dvdslcmf  16601  isprm2lem  16651  eulerthlem2  16752  ramcl2lem  16980  imasvscafn  17500  mreexexlem4d  17608  issgrpd  18657  cycsubgcl  19138  galactghm  19334  odlem2  19469  gexlem2  19512  mulgmhm  19757  mulgghm  19758  gsumval3  19837  gsumpt  19892  dprdfeq0  19954  srglmhm  20130  srgrmhm  20131  ringlghm  20221  ringrghm  20222  sdrgacs  20710  cntzsdrg  20711  lssssr  20860  lbsind  20987  cnsubrg  21344  mplmonmul  21943  mplcoe1  21944  mplcoe5  21947  matplusgcell  22320  elcls  22960  neips  23000  opnnei  23007  ordtbaslem  23075  ptclsg  23502  qtopeu  23603  xmetpsmet  24236  comet  24401  metrest  24412  pcorevlem  24926  dyadmbl  25501  mbfeqalem1  25542  i1fadd  25596  itg1addlem2  25598  itg2uba  25644  itgss  25713  dvcnp  25820  quotval  26200  vieta1lem2  26219  aalioulem3  26242  ulmdvlem3  26311  dvradcnv  26330  abelthlem6  26346  abelthlem9  26350  abelth  26351  logtayllem  26568  logtayl  26569  cxpcl  26583  recxpcl  26584  cxpcn3lem  26657  leibpi  26852  musum  27101  dchrelbas3  27149  sumdchr2  27181  lgscllem  27215  lgsdir2  27241  dchrvmasumiflem2  27413  rpvmasum2  27423  padicabv  27541  padicabvf  27542  padicabvcxp  27543  mulsuniflem  28052  divsval  28092  1wlkdlem4  30069  nmooval  30692  hiidge0  31027  hommval  31665  hfmmval  31668  nmcfnlbi  31981  mdslmd1i  32258  mdslmd3i  32261  sumdmdlem2  32348  foresf1o  32433  disjdifprg  32504  xdivval  32839  nsgqusf1olem2  33385  ply1mulrtss  33550  esumfsupre  34061  dya2iocnei  34273  eulerpartlemgc  34353  eulerpartlemb  34359  eulerpartlemgh  34369  ballotlemfc0  34484  ballotlemfcc  34485  subfacp1lem5  35171  subfacp1lem6  35172  cvmliftlem10  35281  elmrsubrn  35507  colinearperm1  36050  colinearperm5  36054  endofsegid  36073  segcon2  36093  seglecgr12im  36098  segletr  36102  colinbtwnle  36106  broutsideof2  36110  btwnoutside  36113  outsideoftr  36117  outsidele  36120  opnbnd  36313  ctbssinf  37394  matunitlindf  37612  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem19  37633  poimirlem26  37640  heibor1lem  37803  heiborlem3  37807  heiborlem10  37814  ablo4pnp  37874  crngm4  37997  lkrpssN  39156  pclvalN  39884  polvalN  39899  lclkrlem2x  41524  hgmaprnlem5N  41894  aks6d1c2p2  42107  unitscyglem2  42184  selvvvval  42573  fsuppssindlem1  42579  infdesc  42631  onsupmaxb  43228  dvgrat  44301  radcnvrat  44303  sswfaxreg  44977  cncfiooicclem1  45891  fourierdlem101  46205  etransclem24  46256  ioorrnopn  46303  isthincd2  49426