Theorem sylanb 582

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 581	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  599  anabsan  666  rmob  3828  sspsstr  4048  disjne  4395  rexopabb  5483  seex  5590  xpcan2  6141  tron  6346  fcof  6691  fssres  6706  funbrfvb  6893  funopfvb  6894  fvco  6938  fvimacnvi  7004  ffvresb  7078  funressn  7113  funresdfunsn  7144  fvtp2  7151  fvtp2g  7154  fnex  7172  funex  7174  ordsucss  7769  ordsucelsuc  7773  1st2nd  7992  1stconst  8050  2ndconst  8051  frxp  8076  imacosupp  8159  dftpos4  8195  tz7.48lem  8380  nnmsucr  8561  nnmcan  8570  xpmapenlem  9082  php  9141  php4  9144  isfinite2  9208  imafiOLD  9226  fundmfibi  9246  fiinfcl  9416  wofib  9460  r1limg  9695  r1pwcl  9771  cardmin2  9923  zornn0g  10427  mptct  10460  intgru  10737  supsrlem  11034  nzadd  12575  fnn0ind  12628  uztrn2  12807  nnwo  12863  irradd  12923  qbtwnxr  13152  xltnegi  13168  xaddnemnf  13188  xaddnepnf  13189  xaddcom  13192  xnegdi  13200  elioore  13328  uzsubsubfz1  13501  fzo1fzo0n0  13670  elfzonelfzo  13724  modsumfzodifsn  13906  leexp2  14133  faclbnd  14252  faclbnd3  14254  fi1uzind  14469  brfi1uzind  14470  opfi1uzind  14473  swrdccat3b  14702  dvdslelem  16278  divalglem1  16363  dvdsprime  16656  pcgcd  16849  cntri  19307  cntzsgrpcl  19309  efgsrel  19709  xrsdsreclb  21394  znf1o  21531  restuni  23127  stoig  23128  restperf  23149  resstps  23152  pnfnei  23185  mnfnei  23186  cnnei  23247  cmpsublem  23364  comppfsc  23497  tx1stc  23615  xkopt  23620  isfcls  23974  tgioo  24761  opnreen  24797  iscmet3  25260  dyaddisj  25563  limcmpt  25850  degltlem1  26037  ulmdvlem3  26367  lgsdi  27297  noreson  27624  divsclw  28187  cusgrres  29517  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  wwlksnred  29960  eupth2lem3lem4  30301  grpoidinvlem3  30577  ipasslem3  30904  spanuni  31615  5oalem3  31727  5oalem5  31729  mdslmd1lem2  32397  rnressnsn  32750  mptctf  32789  xaddeq0  32826  xnn0gt0  32842  ssdifidllem  33516  ssmxidllem  33533  ssmxidl  33534  ordtconnlem1  34068  esumcvg  34230  ldgenpisyslem1  34307  measdivcst  34368  measdivcstALTV  34369  probun  34563  fnrelpredd  35234  elwf  35240  r1omhf  35249  fineqvrep  35258  elmpps  35755  dfon2lem9  35971  funpartfun  36125  cgrxfr  36237  segcon2  36287  brsegle2  36291  seglecgr12im  36292  segletr  36296  nn0prpw  36505  bj-seex  37229  bj-axreprepsep  37382  bj-prmoore  37427  fvineqsneu  37727  lindsenlbs  37936  matunitlindflem2  37938  ptrecube  37941  poimirlem28  37969  ftc1anclem5  38018  ftc1anc  38022  exlimddvfi  38443  imadomfi  42441  readvrec  42794  nn0addcom  42907  nn0mulcom  42911  riccrng1  42966  ricdrng1  42973  mzpclall  43159  4an31  44925  cnrefiisplem  46257  iundjiun  46888  funbrafvb  47604  funopafvb  47605  afvco2  47624  dfatbrafv2b  47693  funbrafv22b  47698  funopafv2b  47699  sprsymrelfolem2  47953  uhgrimgrlim  48463  line2xlem  49229  itsclc0xyqsol  49244  f1mo  49328  catprs  49486  setrec2lem2  50169