Theorem sylan2br 594

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  syl2anbr  598  pm2.61danel  3054  imainss  6147  funeu2  6568  imadif  6626  fnop  6652  ssimaex  6970  tfindsg2  7848  nn0suc  7883  xpexr2  7909  poxp2  8129  sexp3  8139  extmptsuppeq  8173  suppss  8179  suppssOLD  8180  suppss2  8186  frrlem14  8285  wfr3g  8308  smores3  8354  tfr3ALT  8403  tz7.48-2  8443  swoso  8738  entrfil  9190  domtrfil  9197  1sdom  9250  isinf  9262  isinfOLD  9263  frfi  9290  dffi3  9428  marypha1lem  9430  ordtypelem7  9521  cnfcom2lem  9698  r1pw  9842  rankxplim3  9878  dfac5  10125  cofsmo  10266  axcclem  10454  zorn2lem7  10499  wloglei  11750  divval  11878  uzind3  12660  xrltnsym  13122  xaddf  13209  xrsupsslem  13292  xrinfmsslem  13293  0fz1  13527  hashunsng  14357  hashunsngx  14358  hashgt0elexb  14367  sumss  15676  fsumss  15677  fsumcvg3  15681  abscvgcvg  15771  isumshft  15791  geoisum1  15831  geoisum1c  15832  mertenslem2  15837  zprod  15887  prodss  15897  fprodss  15898  rpnnen2lem5  16168  gcdcllem3  16449  lcmgcd  16551  lcmdvds  16552  lcmfval  16565  lcmfcl  16572  dvdslcmf  16575  isprm2lem  16625  eulerthlem2  16724  ramcl2lem  16951  imasvscafn  17492  mreexexlem4d  17600  issgrpd  18663  cycsubgcl  19132  galactghm  19324  odlem2  19459  gexlem2  19502  mulgmhm  19747  mulgghm  19748  gsumval3  19827  gsumpt  19882  dprdfeq0  19944  srglmhm  20126  srgrmhm  20127  ringlghm  20211  ringrghm  20212  sdrgacs  20652  cntzsdrg  20653  lssssr  20801  lbsind  20928  cnsubrg  21321  mplmonmul  21933  mplcoe1  21934  mplcoe5  21937  matplusgcell  22290  elcls  22932  neips  22972  opnnei  22979  ordtbaslem  23047  ptclsg  23474  qtopeu  23575  xmetpsmet  24209  comet  24377  metrest  24388  pcorevlem  24908  dyadmbl  25484  mbfeqalem1  25525  i1fadd  25579  itg1addlem2  25581  itg2uba  25628  itgss  25696  dvcnp  25803  quotval  26182  vieta1lem2  26201  aalioulem3  26224  ulmdvlem3  26293  dvradcnv  26312  abelthlem6  26328  abelthlem9  26332  abelth  26333  logtayllem  26548  logtayl  26549  cxpcl  26563  recxpcl  26564  cxpcn3lem  26637  leibpi  26829  musum  27078  dchrelbas3  27126  sumdchr2  27158  lgscllem  27192  lgsdir2  27218  dchrvmasumiflem2  27390  rpvmasum2  27400  padicabv  27518  padicabvf  27519  padicabvcxp  27520  mulsuniflem  28004  divsval  28044  1wlkdlem4  29902  nmooval  30525  hiidge0  30860  hommval  31498  hfmmval  31501  nmcfnlbi  31814  mdslmd1i  32091  mdslmd3i  32094  sumdmdlem2  32181  foresf1o  32251  disjdifprg  32315  cnvoprabOLD  32452  xdivval  32590  nsgqusf1olem2  33031  esumfsupre  33599  dya2iocnei  33811  eulerpartlemgc  33891  eulerpartlemb  33897  eulerpartlemgh  33907  ballotlemfc0  34021  ballotlemfcc  34022  subfacp1lem5  34703  subfacp1lem6  34704  cvmliftlem10  34813  elmrsubrn  35039  colinearperm1  35567  colinearperm5  35571  endofsegid  35590  segcon2  35610  seglecgr12im  35615  segletr  35619  colinbtwnle  35623  broutsideof2  35627  btwnoutside  35630  outsideoftr  35634  outsidele  35637  opnbnd  35718  ctbssinf  36794  matunitlindf  36999  poimirlem11  37012  poimirlem12  37013  poimirlem16  37017  poimirlem19  37020  poimirlem26  37027  heibor1lem  37190  heiborlem3  37194  heiborlem10  37201  ablo4pnp  37261  crngm4  37384  lkrpssN  38546  pclvalN  39274  polvalN  39289  lclkrlem2x  40914  hgmaprnlem5N  41284  aks6d1c2p2  41496  selvvvval  41714  fsuppssindlem1  41720  infdesc  41963  onsupmaxb  42564  dvgrat  43647  radcnvrat  43649  cncfiooicclem1  45181  fourierdlem101  45495  etransclem24  45546  ioorrnopn  45593  isthincd2  47932