Theorem sylanb 581

Description: A syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

Ref	Expression
sylanb.1	⊢ (𝜑 ↔ 𝜓)
sylanb.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylanb	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem sylanb

Step	Hyp	Ref	Expression
1		sylanb.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 216	. 2 ⊢ (𝜑 → 𝜓)
3		sylanb.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 580	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:  syl2anb  598  anabsan  665  rmob  3850  sspsstr  4067  disjne  4414  rexopabb  5483  seex  5590  xpcan2  6138  tron  6343  fcof  6693  fssres  6708  funbrfvb  6896  funopfvb  6897  fvco  6941  fvimacnvi  7006  ffvresb  7079  funressn  7113  funresdfunsn  7145  fvtp2  7152  fvtp2g  7155  fnex  7173  funex  7175  ordsucss  7773  ordsucelsuc  7777  1st2nd  7997  1stconst  8056  2ndconst  8057  frxp  8082  imacosupp  8165  dftpos4  8201  tz7.48lem  8386  nnmsucr  8566  nnmcan  8575  xpmapenlem  9085  php  9148  php4  9151  isfinite2  9221  imafiOLD  9241  fundmfibi  9263  fiinfcl  9430  wofib  9474  r1limg  9700  r1pwcl  9776  cardmin2  9928  zornn0g  10434  mptct  10467  intgru  10743  supsrlem  11040  nzadd  12557  fnn0ind  12609  uztrn2  12788  nnwo  12848  irradd  12908  qbtwnxr  13136  xltnegi  13152  xaddnemnf  13172  xaddnepnf  13173  xaddcom  13176  xnegdi  13184  elioore  13312  uzsubsubfz1  13484  fzo1fzo0n0  13652  elfzonelfzo  13706  modsumfzodifsn  13885  leexp2  14112  faclbnd  14231  faclbnd3  14233  fi1uzind  14448  brfi1uzind  14449  opfi1uzind  14452  swrdccat3b  14681  dvdslelem  16255  divalglem1  16340  dvdsprime  16633  pcgcd  16825  cntri  19240  cntzsgrpcl  19242  efgsrel  19640  xrsdsreclb  21306  znf1o  21437  restuni  23025  stoig  23026  restperf  23047  resstps  23050  pnfnei  23083  mnfnei  23084  cnnei  23145  cmpsublem  23262  comppfsc  23395  tx1stc  23513  xkopt  23518  isfcls  23872  tgioo  24660  opnreen  24696  iscmet3  25169  dyaddisj  25473  limcmpt  25760  degltlem1  25953  ulmdvlem3  26287  lgsdi  27221  noreson  27548  divsclw  28074  cusgrres  29352  crctcshwlkn0lem4  29716  crctcshwlkn0lem5  29717  wwlksnred  29795  eupth2lem3lem4  30133  grpoidinvlem3  30408  ipasslem3  30735  spanuni  31446  5oalem3  31558  5oalem5  31560  mdslmd1lem2  32228  mptctf  32614  xaddeq0  32649  xnn0gt0  32665  ssdifidllem  33400  ssmxidllem  33417  ssmxidl  33418  ordtconnlem1  33887  esumcvg  34049  ldgenpisyslem1  34126  measdivcst  34187  measdivcstALTV  34188  probun  34383  fnrelpredd  35052  fineqvrep  35058  elmpps  35533  dfon2lem9  35752  funpartfun  35904  cgrxfr  36016  segcon2  36066  brsegle2  36070  seglecgr12im  36071  segletr  36075  nn0prpw  36284  bj-seex  36883  bj-prmoore  37076  fvineqsneu  37372  lindsenlbs  37582  matunitlindflem2  37584  ptrecube  37587  poimirlem28  37615  ftc1anclem5  37664  ftc1anc  37668  exlimddvfi  38089  imadomfi  41963  readvrec  42323  nn0addcom  42423  nn0mulcom  42427  riccrng1  42482  ricdrng1  42489  mzpclall  42688  4an31  44461  cnrefiisplem  45800  iundjiun  46431  funbrafvb  47130  funopafvb  47131  afvco2  47150  dfatbrafv2b  47219  funbrafv22b  47224  funopafv2b  47225  sprsymrelfolem2  47467  uhgrimgrlim  47959  line2xlem  48715  itsclc0xyqsol  48730  f1mo  48814  catprs  48973  setrec2lem2  49656