Theorem sylanb 579

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 578	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 395

This theorem is referenced by:  syl2anb  596  anabsan  661  eqtr2OLD  2755  pm13.181OLD  3022  rmob  3883  sspsstr  4104  disjne  4453  rexopabb  5527  seex  5637  xpcan2  6175  tron  6386  fcof  6739  fssres  6756  funbrfvb  6945  funopfvb  6946  fvco  6988  fvimacnvi  7052  ffvresb  7125  funressn  7158  funresdfunsn  7188  fvtp2  7198  fvtp2g  7201  fnex  7220  funex  7222  ordsucss  7808  ordsucelsuc  7812  1st2nd  8027  1stconst  8088  2ndconst  8089  frxp  8114  imacosupp  8196  dftpos4  8232  tz7.48lem  8443  nnmsucr  8627  nnmcan  8636  xpmapenlem  9146  imafi  9177  php  9212  php4  9215  phpOLD  9224  isfinite2  9303  fundmfibi  9333  fiinfcl  9498  wofib  9542  r1limg  9768  r1pwcl  9844  cardmin2  9996  zornn0g  10502  mptct  10535  intgru  10811  supsrlem  11108  nzadd  12614  fnn0ind  12665  uztrn2  12845  nnwo  12901  irradd  12961  qbtwnxr  13183  xltnegi  13199  xaddnemnf  13219  xaddnepnf  13220  xaddcom  13223  xnegdi  13231  elioore  13358  uzsubsubfz1  13528  fzo1fzo0n0  13687  elfzonelfzo  13738  modsumfzodifsn  13913  leexp2  14140  faclbnd  14254  faclbnd3  14256  fi1uzind  14462  brfi1uzind  14463  opfi1uzind  14466  swrdccat3b  14694  dvdslelem  16256  divalglem1  16341  dvdsprime  16628  pcgcd  16815  cntri  19237  cntzsgrpcl  19239  efgsrel  19643  xrsdsreclb  21192  znf1o  21326  restuni  22886  stoig  22887  restperf  22908  resstps  22911  pnfnei  22944  mnfnei  22945  cnnei  23006  cmpsublem  23123  comppfsc  23256  tx1stc  23374  xkopt  23379  isfcls  23733  tgioo  24532  opnreen  24567  iscmet3  25041  dyaddisj  25345  limcmpt  25632  degltlem1  25825  ulmdvlem3  26150  lgsdi  27073  noreson  27399  divsclw  27881  cusgrres  28972  crctcshwlkn0lem4  29334  crctcshwlkn0lem5  29335  wwlksnred  29413  eupth2lem3lem4  29751  grpoidinvlem3  30026  ipasslem3  30353  spanuni  31064  5oalem3  31176  5oalem5  31178  mdslmd1lem2  31846  mptctf  32209  xaddeq0  32233  xnn0gt0  32249  ssmxidllem  32863  ssmxidl  32864  ordtconnlem1  33202  esumcvg  33382  ldgenpisyslem1  33459  measdivcst  33520  measdivcstALTV  33521  probun  33716  fnrelpredd  34390  fineqvrep  34393  elmpps  34862  dfon2lem9  35067  funpartfun  35219  cgrxfr  35331  segcon2  35381  brsegle2  35385  seglecgr12im  35386  segletr  35390  nn0prpw  35511  bj-seex  36105  bj-prmoore  36299  fvineqsneu  36595  lindsenlbs  36786  matunitlindflem2  36788  ptrecube  36791  poimirlem28  36819  ftc1anclem5  36868  ftc1anc  36872  exlimddvfi  37293  riccrng1  41400  ricdrng1  41406  nn0addcom  41625  nn0mulcom  41629  mzpclall  41767  4an31  43561  cnrefiisplem  44843  iundjiun  45474  funbrafvb  46162  funopafvb  46163  afvco2  46182  dfatbrafv2b  46251  funbrafv22b  46256  funopafv2b  46257  sprsymrelfolem2  46459  line2xlem  47526  itsclc0xyqsol  47541  f1mo  47606  catprs  47718  setrec2lem2  47826