Theorem sylan2br 604

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ 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 209  df-an 400

This theorem is referenced by:  syl2anbr  608  pm2.61danel  3077  imainss  6141  funeu2  6549  imadif  6607  fnop  6632  ssimaex  6954  tfindsg2  7844  nn0suc  7877  xpexr2  7902  poxp2  8125  sexp3  8135  extmptsuppeq  8170  suppss  8176  suppss2  8182  frrlem14  8282  wfr3g  8302  smores3  8326  tfr3ALT  8375  tz7.48-2  8415  swoso  8715  entrfil  9155  domtrfil  9162  1sdom  9201  isinf  9211  frfi  9231  dffi3  9379  marypha1lem  9381  ordtypelem7  9474  cnfcom2lem  9658  r1pw  9805  rankxplim3  9841  dfac5  10087  cofsmo  10228  axcclem  10416  zorn2lem7  10461  wloglei  11721  divval  11849  uzind3  12669  xrltnsym  13141  xaddf  13229  xrsupsslem  13312  xrinfmsslem  13313  0fz1  13551  hashunsng  14407  hashunsngx  14408  hashgt0elexb  14417  sumss  15753  fsumss  15754  fsumcvg3  15758  abscvgcvg  15849  isumshft  15871  geoisum1  15911  geoisum1c  15912  mertenslem2  15917  zprod  15969  prodss  15979  fprodss  15980  rpnnen2lem5  16252  gcdcllem3  16537  lcmgcd  16643  lcmdvds  16644  lcmfval  16657  lcmfcl  16664  dvdslcmf  16667  isprm2lem  16717  eulerthlem2  16819  ramcl2lem  17047  imasvscafn  17569  mreexexlem4d  17681  issgrpd  18766  cycsubgcl  19249  galactghm  19446  odlem2  19581  gexlem2  19624  mulgmhm  19869  mulgghm  19870  gsumval3  19949  gsumpt  20004  dprdfeq0  20066  srglmhm  20273  srgrmhm  20274  ringlghm  20364  ringrghm  20365  sdrgacs  20852  cntzsdrg  20853  lssssr  21023  lbsind  21149  cnsubrg  21481  mplmonmul  22091  mplcoe1  22092  mplcoe5  22095  selvvvval  22197  matplusgcell  22495  elcls  23135  neips  23175  opnnei  23182  ordtbaslem  23250  ptclsg  23677  qtopeu  23778  xmetpsmet  24410  comet  24575  metrest  24586  pcorevlem  25090  dyadmbl  25664  mbfeqalem1  25705  i1fadd  25759  itg1addlem2  25761  itg2uba  25807  itgss  25876  dvcnp  25983  quotval  26358  vieta1lem2  26377  aalioulem3  26400  ulmdvlem3  26467  dvradcnv  26486  abelthlem6  26501  abelthlem9  26505  abelth  26506  logtayllem  26726  logtayl  26727  cxpcl  26741  recxpcl  26742  cxpcn3lem  26814  leibpi  27009  musum  27257  dchrelbas3  27304  sumdchr2  27336  lgscllem  27370  lgsdir2  27396  dchrvmasumiflem2  27568  rpvmasum2  27578  padicabv  27696  padicabvf  27697  padicabvcxp  27698  mulsuniflem  28244  divsval  28284  1wlkdlem4  30344  nmooval  30968  hiidge0  31303  hommval  31941  hfmmval  31944  nmcfnlbi  32257  mdslmd1i  32534  mdslmd3i  32537  sumdmdlem2  32624  foresf1o  32705  disjdifprg  32777  xdivval  33098  nsgqusf1olem2  33602  ply1mulrtss  33780  psrmonmul  33849  esumfsupre  34370  dya2iocnei  34581  eulerpartlemgc  34661  eulerpartlemb  34667  eulerpartlemgh  34677  ballotlemfc0  34792  ballotlemfcc  34793  subfacp1lem5  35539  subfacp1lem6  35540  cvmliftlem10  35649  elmrsubrn  35875  colinearperm1  36417  colinearperm5  36421  endofsegid  36440  segcon2  36460  seglecgr12im  36465  segletr  36469  colinbtwnle  36473  broutsideof2  36477  btwnoutside  36480  outsideoftr  36484  outsidele  36487  opnbnd  36690  ctbssinf  37905  matunitlindf  38122  poimirlem11  38135  poimirlem12  38136  poimirlem16  38140  poimirlem19  38143  poimirlem26  38150  heibor1lem  38313  heiborlem3  38317  heiborlem10  38324  ablo4pnp  38384  crngm4  38507  lkrpssN  39792  pclvalN  40519  polvalN  40534  lclkrlem2x  42159  hgmaprnlem5N  42529  aks6d1c2p2  42741  unitscyglem2  42818  fsuppssindlem1  43178  infdesc  43230  onsupmaxb  43821  dvgrat  44893  radcnvrat  44895  sswfaxreg  45568  cncfiooicclem1  46472  fourierdlem101  46786  etransclem24  46837  ioorrnopn  46884  indprm  48243  isthincd2  50063