Theorem sylanb 489

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 206	. 2 ⊢ (𝜑 → 𝜓)
3		sylanb.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 488	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  syl2anb  496  anabsan  854  eqtr2  2642  pm13.181  2876  rmob  3529  sspsstr  3712  disjne  4022  seex  5077  xpcan2  5571  tron  5746  fssres  6070  funbrfvb  6238  funopfvb  6239  fvco  6274  fvimacnvi  6331  ffvresb  6394  funressn  6426  funresdfunsn  6455  fvtp2  6461  fvtp2g  6464  fnex  6481  funex  6482  ordsucss  7018  ordsucelsuc  7022  1st2nd  7214  frxp  7287  dftpos4  7371  tz7.48lem  7536  nnmsucr  7705  nnmcan  7714  xpmapenlem  8127  php  8144  php4  8147  isfinite2  8218  fundmfibi  8245  fiinfcl  8407  wofib  8450  r1limg  8634  r1pwcl  8710  cardmin2  8824  zornn0g  9327  mptct  9360  intgru  9636  supsrlem  9932  nzadd  11425  fnn0ind  11476  uztrn2  11705  nnwo  11753  irradd  11812  qbtwnxr  12031  xltnegi  12047  xaddnemnf  12067  xaddnepnf  12068  xaddcom  12071  xnegdi  12078  elioore  12205  uzsubsubfz1  12364  fzo1fzo0n0  12518  elfzonelfzo  12570  modsumfzodifsn  12743  leexp2  12915  faclbnd  13077  faclbnd3  13079  fi1uzind  13279  brfi1uzind  13280  opfi1uzind  13283  fi1uzindOLD  13285  brfi1uzindOLD  13286  opfi1uzindOLD  13289  swrdccat3b  13496  dvdslelem  15031  divalglem1  15117  dvdsprime  15400  pcgcd  15582  cntri  17763  efgsrel  18147  xrsdsreclb  19793  znf1o  19900  restuni  20966  stoig  20967  restperf  20988  resstps  20991  pnfnei  21024  mnfnei  21025  cnnei  21086  cmpsublem  21202  comppfsc  21335  tx1stc  21453  xkopt  21458  isfcls  21813  tgioo  22599  opnreen  22634  iscmet3  23091  dyaddisj  23364  limcmpt  23647  degltlem1  23832  ulmdvlem3  24156  lgsdi  25059  cusgrres  26344  crctcshwlkn0lem4  26705  crctcshwlkn0lem5  26706  wwlksnred  26787  clwlksfclwwlk  26962  eupth2lem3lem4  27091  grpoidinvlem3  27360  ipasslem3  27688  spanuni  28403  5oalem3  28515  5oalem5  28517  mdslmd1lem2  29185  mptctf  29495  xaddeq0  29518  ordtconnlem1  29970  esumcvg  30148  ldgenpisyslem1  30226  measres  30285  measdivcstOLD  30287  measdivcst  30288  probun  30481  elmpps  31470  dfon2lem9  31696  noreson  31813  funpartfun  32050  cgrxfr  32162  segcon2  32212  brsegle2  32216  seglecgr12im  32217  segletr  32221  nn0prpw  32318  bj-seex  32919  lindsenlbs  33404  matunitlindflem2  33406  ptrecube  33409  poimirlem28  33437  ftc1anclem5  33489  ftc1anc  33493  exlimddvfi  33927  prtlem11  34151  mzpclall  37290  4an31  38704  cnrefiisplem  40055  iundjiun  40677  funbrafvb  41236  funopafvb  41237  afvco2  41256  sprsymrelfolem2  41743