Theorem sylan2br 602

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 600	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜃)

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

This theorem is referenced by:  syl2anbr  606  pm2.61danel  3054  imainss  6109  funeu2  6515  imadif  6573  fnop  6598  ssimaex  6916  tfindsg2  7806  nn0suc  7838  xpexr2  7863  poxp2  8087  sexp3  8097  extmptsuppeq  8132  suppss  8138  suppss2  8144  frrlem14  8243  wfr3g  8263  smores3  8287  tfr3ALT  8335  tz7.48-2  8375  swoso  8672  entrfil  9113  domtrfil  9120  1sdom  9159  isinf  9169  frfi  9189  dffi3  9338  marypha1lem  9340  ordtypelem7  9433  cnfcom2lem  9617  r1pw  9764  rankxplim3  9800  dfac5  10046  cofsmo  10186  axcclem  10374  zorn2lem7  10419  wloglei  11677  divval  11806  uzind3  12618  xrltnsym  13083  xaddf  13171  xrsupsslem  13254  xrinfmsslem  13255  0fz1  13493  hashunsng  14349  hashunsngx  14350  hashgt0elexb  14359  sumss  15681  fsumss  15682  fsumcvg3  15686  abscvgcvg  15777  isumshft  15799  geoisum1  15839  geoisum1c  15840  mertenslem2  15845  zprod  15897  prodss  15907  fprodss  15908  rpnnen2lem5  16180  gcdcllem3  16465  lcmgcd  16571  lcmdvds  16572  lcmfval  16585  lcmfcl  16592  dvdslcmf  16595  isprm2lem  16645  eulerthlem2  16747  ramcl2lem  16975  imasvscafn  17496  mreexexlem4d  17608  issgrpd  18693  cycsubgcl  19176  galactghm  19374  odlem2  19509  gexlem2  19552  mulgmhm  19797  mulgghm  19798  gsumval3  19877  gsumpt  19932  dprdfeq0  19994  srglmhm  20197  srgrmhm  20198  ringlghm  20288  ringrghm  20289  sdrgacs  20777  cntzsdrg  20778  lssssr  20948  lbsind  21074  cnsubrg  21406  mplmonmul  22016  mplcoe1  22017  mplcoe5  22020  selvvvval  22122  matplusgcell  22420  elcls  23060  neips  23100  opnnei  23107  ordtbaslem  23175  ptclsg  23602  qtopeu  23703  xmetpsmet  24335  comet  24500  metrest  24511  pcorevlem  25015  dyadmbl  25589  mbfeqalem1  25630  i1fadd  25684  itg1addlem2  25686  itg2uba  25732  itgss  25801  dvcnp  25908  quotval  26280  vieta1lem2  26299  aalioulem3  26322  ulmdvlem3  26389  dvradcnv  26408  abelthlem6  26423  abelthlem9  26427  abelth  26428  logtayllem  26645  logtayl  26646  cxpcl  26660  recxpcl  26661  cxpcn3lem  26733  leibpi  26928  musum  27176  dchrelbas3  27223  sumdchr2  27255  lgscllem  27289  lgsdir2  27315  dchrvmasumiflem2  27487  rpvmasum2  27497  padicabv  27615  padicabvf  27616  padicabvcxp  27617  mulsuniflem  28163  divsval  28203  1wlkdlem4  30232  nmooval  30856  hiidge0  31191  hommval  31829  hfmmval  31832  nmcfnlbi  32145  mdslmd1i  32422  mdslmd3i  32425  sumdmdlem2  32512  foresf1o  32596  disjdifprg  32668  xdivval  33001  nsgqusf1olem2  33501  ply1mulrtss  33677  psrmonmul  33746  esumfsupre  34267  dya2iocnei  34478  eulerpartlemgc  34558  eulerpartlemb  34564  eulerpartlemgh  34574  ballotlemfc0  34689  ballotlemfcc  34690  subfacp1lem5  35427  subfacp1lem6  35428  cvmliftlem10  35537  elmrsubrn  35763  colinearperm1  36305  colinearperm5  36309  endofsegid  36328  segcon2  36348  seglecgr12im  36353  segletr  36357  colinbtwnle  36361  broutsideof2  36365  btwnoutside  36368  outsideoftr  36372  outsidele  36375  opnbnd  36568  ctbssinf  37783  matunitlindf  38000  poimirlem11  38013  poimirlem12  38014  poimirlem16  38018  poimirlem19  38021  poimirlem26  38028  heibor1lem  38191  heiborlem3  38195  heiborlem10  38202  ablo4pnp  38262  crngm4  38385  lkrpssN  39670  pclvalN  40397  polvalN  40412  lclkrlem2x  42037  hgmaprnlem5N  42407  aks6d1c2p2  42619  unitscyglem2  42696  fsuppssindlem1  43056  infdesc  43108  onsupmaxb  43699  dvgrat  44771  radcnvrat  44773  sswfaxreg  45446  cncfiooicclem1  46350  fourierdlem101  46664  etransclem24  46715  ioorrnopn  46762  indprm  48121  isthincd2  49941