Theorem sylanb 580

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 215	. 2 ⊢ (𝜑 → 𝜓)
3		sylanb.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 579	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:  syl2anb  597  anabsan  661  eqtr2OLD  2763  pm13.181OLD  3026  rmob  3819  sspsstr  4036  disjne  4385  rexopabb  5434  seex  5542  xpcan2  6069  tron  6274  fcof  6607  fssres  6624  funbrfvb  6806  funopfvb  6807  fvco  6848  fvimacnvi  6911  ffvresb  6980  funressn  7013  funresdfunsn  7043  fvtp2  7053  fvtp2g  7056  fnex  7075  funex  7077  ordsucss  7640  ordsucelsuc  7644  1st2nd  7853  1stconst  7911  2ndconst  7912  frxp  7938  imacosupp  7996  dftpos4  8032  tz7.48lem  8242  nnmsucr  8418  nnmcan  8427  xpmapenlem  8880  php  8897  php4  8900  imafi  8920  isfinite2  9002  fundmfibi  9028  fiinfcl  9190  wofib  9234  r1limg  9460  r1pwcl  9536  cardmin2  9688  zornn0g  10192  mptct  10225  intgru  10501  supsrlem  10798  nzadd  12298  fnn0ind  12349  uztrn2  12530  nnwo  12582  irradd  12642  qbtwnxr  12863  xltnegi  12879  xaddnemnf  12899  xaddnepnf  12900  xaddcom  12903  xnegdi  12911  elioore  13038  uzsubsubfz1  13208  fzo1fzo0n0  13366  elfzonelfzo  13417  modsumfzodifsn  13592  leexp2  13817  faclbnd  13932  faclbnd3  13934  fi1uzind  14139  brfi1uzind  14140  opfi1uzind  14143  swrdccat3b  14381  dvdslelem  15946  divalglem1  16031  dvdsprime  16320  pcgcd  16507  cntri  18852  efgsrel  19255  xrsdsreclb  20557  znf1o  20671  restuni  22221  stoig  22222  restperf  22243  resstps  22246  pnfnei  22279  mnfnei  22280  cnnei  22341  cmpsublem  22458  comppfsc  22591  tx1stc  22709  xkopt  22714  isfcls  23068  tgioo  23865  opnreen  23900  iscmet3  24362  dyaddisj  24665  limcmpt  24952  degltlem1  25142  ulmdvlem3  25466  lgsdi  26387  cusgrres  27718  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  wwlksnred  28158  eupth2lem3lem4  28496  grpoidinvlem3  28769  ipasslem3  29096  spanuni  29807  5oalem3  29919  5oalem5  29921  mdslmd1lem2  30589  mptctf  30954  xaddeq0  30978  xnn0gt0  30994  ssmxidllem  31543  ssmxidl  31544  ordtconnlem1  31776  esumcvg  31954  ldgenpisyslem1  32031  measdivcst  32092  measdivcstALTV  32093  probun  32286  fnrelpredd  32961  fineqvrep  32964  elmpps  33435  dfon2lem9  33673  noreson  33790  funpartfun  34172  cgrxfr  34284  segcon2  34334  brsegle2  34338  seglecgr12im  34339  segletr  34343  nn0prpw  34439  bj-seex  35037  bj-prmoore  35213  fvineqsneu  35509  lindsenlbs  35699  matunitlindflem2  35701  ptrecube  35704  poimirlem28  35732  ftc1anclem5  35781  ftc1anc  35785  exlimddvfi  36207  mzpclall  40465  4an31  42007  cnrefiisplem  43260  iundjiun  43888  funbrafvb  44535  funopafvb  44536  afvco2  44555  dfatbrafv2b  44624  funbrafv22b  44629  funopafv2b  44630  sprsymrelfolem2  44833  line2xlem  45987  itsclc0xyqsol  46002  f1mo  46068  catprs  46180  setrec2lem2  46286