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  eqtr2OLD  2759  pm13.181OLD  3021  rmob  3898  sspsstr  4117  disjne  4460  rexopabb  5537  seex  5647  xpcan2  6198  tron  6408  fcof  6759  fssres  6774  funbrfvb  6961  funopfvb  6962  fvco  7006  fvimacnvi  7071  ffvresb  7144  funressn  7178  funresdfunsn  7208  fvtp2  7215  fvtp2g  7218  fnex  7236  funex  7238  ordsucss  7837  ordsucelsuc  7841  1st2nd  8062  1stconst  8123  2ndconst  8124  frxp  8149  imacosupp  8232  dftpos4  8268  tz7.48lem  8479  nnmsucr  8661  nnmcan  8670  xpmapenlem  9182  php  9244  php4  9247  phpOLD  9256  isfinite2  9331  imafiOLD  9351  fundmfibi  9373  fiinfcl  9538  wofib  9582  r1limg  9808  r1pwcl  9884  cardmin2  10036  zornn0g  10542  mptct  10575  intgru  10851  supsrlem  11148  nzadd  12662  fnn0ind  12714  uztrn2  12894  nnwo  12952  irradd  13012  qbtwnxr  13238  xltnegi  13254  xaddnemnf  13274  xaddnepnf  13275  xaddcom  13278  xnegdi  13286  elioore  13413  uzsubsubfz1  13583  fzo1fzo0n0  13750  elfzonelfzo  13804  modsumfzodifsn  13981  leexp2  14207  faclbnd  14325  faclbnd3  14327  fi1uzind  14542  brfi1uzind  14543  opfi1uzind  14546  swrdccat3b  14774  dvdslelem  16342  divalglem1  16427  dvdsprime  16720  pcgcd  16911  cntri  19362  cntzsgrpcl  19364  efgsrel  19766  xrsdsreclb  21448  znf1o  21587  restuni  23185  stoig  23186  restperf  23207  resstps  23210  pnfnei  23243  mnfnei  23244  cnnei  23305  cmpsublem  23422  comppfsc  23555  tx1stc  23673  xkopt  23678  isfcls  24032  tgioo  24831  opnreen  24866  iscmet3  25340  dyaddisj  25644  limcmpt  25932  degltlem1  26125  ulmdvlem3  26459  lgsdi  27392  noreson  27719  divsclw  28234  cusgrres  29480  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  wwlksnred  29921  eupth2lem3lem4  30259  grpoidinvlem3  30534  ipasslem3  30861  spanuni  31572  5oalem3  31684  5oalem5  31686  mdslmd1lem2  32354  mptctf  32734  xaddeq0  32763  xnn0gt0  32779  ssdifidllem  33463  ssmxidllem  33480  ssmxidl  33481  ordtconnlem1  33884  esumcvg  34066  ldgenpisyslem1  34143  measdivcst  34204  measdivcstALTV  34205  probun  34400  fnrelpredd  35081  fineqvrep  35087  elmpps  35557  dfon2lem9  35772  funpartfun  35924  cgrxfr  36036  segcon2  36086  brsegle2  36090  seglecgr12im  36091  segletr  36095  nn0prpw  36305  bj-seex  36904  bj-prmoore  37097  fvineqsneu  37393  lindsenlbs  37601  matunitlindflem2  37603  ptrecube  37606  poimirlem28  37634  ftc1anclem5  37683  ftc1anc  37687  exlimddvfi  38108  imadomfi  41983  readvrec  42370  nn0addcom  42456  nn0mulcom  42460  riccrng1  42507  ricdrng1  42514  mzpclall  42714  4an31  44495  cnrefiisplem  45784  iundjiun  46415  funbrafvb  47105  funopafvb  47106  afvco2  47125  dfatbrafv2b  47194  funbrafv22b  47199  funopafv2b  47200  sprsymrelfolem2  47417  uhgrimgrlim  47889  line2xlem  48602  itsclc0xyqsol  48617  f1mo  48682  catprs  48799  setrec2lem2  48924