Theorem sylan2br 607

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  syl2anbr  611  pm2.61danel  3075  imainss  6146  funeu2  6561  imadif  6619  fnop  6643  ssimaex  6965  tfindsg2  7860  nn0suc  7893  xpexr2  7918  poxp2  8143  sexp3  8153  extmptsuppeq  8188  suppss  8194  suppss2  8200  frrlem14  8300  wfr3g  8320  smores3  8344  tfr3ALT  8393  tz7.48-2  8435  swoso  8735  entrfil  9183  domtrfil  9190  1sdom  9229  isinf  9239  frfi  9259  dffi3  9405  marypha1lem  9407  ordtypelem7  9500  cnfcom2lem  9684  r1pw  9833  rankxplim3  9871  dfac5  10153  cofsmo  10293  axcclem  10481  zorn2lem7  10526  wloglei  11792  divval  11920  uzind3  12737  xrltnsym  13210  xaddf  13298  xrsupsslem  13381  xrinfmsslem  13382  0fz1  13620  hashunsng  14478  hashunsngx  14479  hashgt0elexb  14488  sumss  15832  fsumss  15833  fsumcvg3  15837  abscvgcvg  15928  isumshft  15950  geoisum1  15990  geoisum1c  15991  mertenslem2  15996  zprod  16046  prodss  16056  fprodss  16057  rpnnen2lem5  16328  gcdcllem3  16613  lcmgcd  16719  lcmdvds  16720  lcmfval  16733  lcmfcl  16740  dvdslcmf  16743  isprm2lem  16793  eulerthlem2  16895  ramcl2lem  17123  imasvscafn  17645  mreexexlem4d  17757  issgrpd  18855  cycsubgcl  19357  galactghm  19554  odlem2  19689  gexlem2  19732  mulgmhm  19977  mulgghm  19978  gsumval3  20057  gsumpt  20112  dprdfeq0  20174  srglmhm  20383  srgrmhm  20384  ringlghm  20479  ringrghm  20480  sdrgacs  20994  cntzsdrg  20995  lssssr  21165  lbsind  21291  cnsubrg  21669  mplmonmul  22281  mplcoe1  22282  mplcoe5  22285  selvvvval  22387  matplusgcell  22684  matunitlindf  22932  elcls  23327  neips  23367  opnnei  23374  ordtbaslem  23442  ptclsg  23870  qtopeu  23971  xmetpsmet  24603  comet  24768  metrest  24779  pcorevlem  25283  dyadmbl  25857  mbfeqalem1  25898  i1fadd  25952  itg1addlem2  25954  itg2uba  26000  itgss  26068  dvcnp  26175  quotval  26551  vieta1lem2  26572  aalioulem3  26599  ulmdvlem3  26667  dvradcnv  26686  abelthlem6  26701  abelthlem9  26705  abelth  26706  logtayllem  26925  logtayl  26926  cxpcl  26940  recxpcl  26941  cxpcn3lem  27013  leibpi  27208  musum  27456  dchrelbas3  27503  sumdchr2  27535  lgscllem  27569  lgsdir2  27595  dchrvmasumiflem2  27767  rpvmasum2  27777  padicabv  27895  padicabvf  27896  padicabvcxp  27897  mulsuniflem  28443  divsval  28483  1wlkdlem4  30639  nmooval  31273  hiidge0  31608  hommval  32246  hfmmval  32249  nmcfnlbi  32562  mdslmd1i  32839  mdslmd3i  32842  sumdmdlem2  32929  foresf1o  33008  disjdifprg  33077  xdivval  33393  nsgqusf1olem2  33873  ply1mulrtss  34022  psrmonmul  34090  esumfsupre  34611  dya2iocnei  34823  eulerpartlemgc  34903  eulerpartlemb  34909  eulerpartlemgh  34919  ballotlemfc0  35034  ballotlemfcc  35035  subfacp1lem5  35793  subfacp1lem6  35794  cvmliftlem10  35903  elmrsubrn  36129  colinearperm1  36672  colinearperm5  36676  endofsegid  36695  segcon2  36715  seglecgr12im  36720  segletr  36724  colinbtwnle  36728  broutsideof2  36732  btwnoutside  36735  outsideoftr  36739  outsidele  36742  opnbnd  36958  ctbssinf  38174  poimirlem11  38394  poimirlem12  38395  poimirlem16  38399  poimirlem19  38402  poimirlem26  38409  heibor1lem  38573  heiborlem3  38577  heiborlem10  38584  ablo4pnp  38644  crngm4  38767  lkrpssN  40050  pclvalN  40777  polvalN  40792  lclkrlem2x  42417  hgmaprnlem5N  42787  aks6d1c2p2  42999  unitscyglem2  43076  fsuppssindlem1  43451  infdesc  43503  onsupmaxb  44094  dvgrat  45150  radcnvrat  45152  sswfaxreg  45824  cncfiooicclem1  46735  fourierdlem101  47049  etransclem24  47100  ioorrnopn  47147  indprm  48546  isthincd2  50377