Theorem sylan2br 596

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 594	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  600  pm2.61danel  3050  imainss  6118  funeu2  6524  imadif  6582  fnop  6607  ssimaex  6925  tfindsg2  7813  nn0suc  7845  xpexr2  7870  poxp2  8093  sexp3  8103  extmptsuppeq  8138  suppss  8144  suppss2  8150  frrlem14  8249  wfr3g  8269  smores3  8293  tfr3ALT  8341  tz7.48-2  8381  swoso  8678  entrfil  9119  domtrfil  9126  1sdom  9165  isinf  9175  frfi  9195  dffi3  9344  marypha1lem  9346  ordtypelem7  9439  cnfcom2lem  9622  r1pw  9769  rankxplim3  9805  dfac5  10051  cofsmo  10191  axcclem  10379  zorn2lem7  10424  wloglei  11682  divval  11811  uzind3  12623  xrltnsym  13088  xaddf  13176  xrsupsslem  13259  xrinfmsslem  13260  0fz1  13498  hashunsng  14354  hashunsngx  14355  hashgt0elexb  14364  sumss  15686  fsumss  15687  fsumcvg3  15691  abscvgcvg  15782  isumshft  15804  geoisum1  15844  geoisum1c  15845  mertenslem2  15850  zprod  15902  prodss  15912  fprodss  15913  rpnnen2lem5  16185  gcdcllem3  16470  lcmgcd  16576  lcmdvds  16577  lcmfval  16590  lcmfcl  16597  dvdslcmf  16600  isprm2lem  16650  eulerthlem2  16752  ramcl2lem  16980  imasvscafn  17501  mreexexlem4d  17613  issgrpd  18698  cycsubgcl  19181  galactghm  19379  odlem2  19514  gexlem2  19557  mulgmhm  19802  mulgghm  19803  gsumval3  19882  gsumpt  19937  dprdfeq0  19999  srglmhm  20202  srgrmhm  20203  ringlghm  20293  ringrghm  20294  sdrgacs  20778  cntzsdrg  20779  lssssr  20949  lbsind  21075  cnsubrg  21407  mplmonmul  22014  mplcoe1  22015  mplcoe5  22018  matplusgcell  22398  elcls  23038  neips  23078  opnnei  23085  ordtbaslem  23153  ptclsg  23580  qtopeu  23681  xmetpsmet  24313  comet  24478  metrest  24489  pcorevlem  24993  dyadmbl  25567  mbfeqalem1  25608  i1fadd  25662  itg1addlem2  25664  itg2uba  25710  itgss  25779  dvcnp  25886  quotval  26258  vieta1lem2  26277  aalioulem3  26300  ulmdvlem3  26367  dvradcnv  26386  abelthlem6  26401  abelthlem9  26405  abelth  26406  logtayllem  26623  logtayl  26624  cxpcl  26638  recxpcl  26639  cxpcn3lem  26711  leibpi  26906  musum  27154  dchrelbas3  27201  sumdchr2  27233  lgscllem  27267  lgsdir2  27293  dchrvmasumiflem2  27465  rpvmasum2  27475  padicabv  27593  padicabvf  27594  padicabvcxp  27595  mulsuniflem  28141  divsval  28181  1wlkdlem4  30210  nmooval  30834  hiidge0  31169  hommval  31807  hfmmval  31810  nmcfnlbi  32123  mdslmd1i  32400  mdslmd3i  32403  sumdmdlem2  32490  foresf1o  32574  disjdifprg  32645  xdivval  32978  nsgqusf1olem2  33474  ply1mulrtss  33642  psrmonmul  33694  esumfsupre  34215  dya2iocnei  34426  eulerpartlemgc  34506  eulerpartlemb  34512  eulerpartlemgh  34522  ballotlemfc0  34637  ballotlemfcc  34638  subfacp1lem5  35366  subfacp1lem6  35367  cvmliftlem10  35476  elmrsubrn  35702  colinearperm1  36244  colinearperm5  36248  endofsegid  36267  segcon2  36287  seglecgr12im  36292  segletr  36296  colinbtwnle  36300  broutsideof2  36304  btwnoutside  36307  outsideoftr  36311  outsidele  36314  opnbnd  36507  ctbssinf  37722  matunitlindf  37939  poimirlem11  37952  poimirlem12  37953  poimirlem16  37957  poimirlem19  37960  poimirlem26  37967  heibor1lem  38130  heiborlem3  38134  heiborlem10  38141  ablo4pnp  38201  crngm4  38324  lkrpssN  39609  pclvalN  40336  polvalN  40351  lclkrlem2x  41976  hgmaprnlem5N  42346  aks6d1c2p2  42558  unitscyglem2  42635  selvvvval  43018  fsuppssindlem1  43024  infdesc  43076  onsupmaxb  43667  dvgrat  44739  radcnvrat  44741  sswfaxreg  45414  cncfiooicclem1  46321  fourierdlem101  46635  etransclem24  46686  ioorrnopn  46733  indprm  48092  isthincd2  49912