Theorem sylanb 590

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  syl2anb  607  anabsan  675  rmob  3841  sspsstr  4060  disjne  4406  rexopabb  5495  seex  5602  xpcan2  6158  tron  6364  fcof  6710  fssres  6725  funbrfvb  6915  funopfvb  6916  fvco  6960  fvimacnvi  7028  ffvresb  7102  funressn  7137  funresdfunsn  7168  fvtp2  7175  fvtp2g  7178  fnex  7196  funex  7198  ordsucss  7793  ordsucelsuc  7797  1st2nd  8015  1stconst  8073  2ndconst  8074  frxp  8100  imacosupp  8183  dftpos4  8219  tz7.48lem  8406  nnmsucr  8589  nnmcan  8598  xpmapenlem  9110  php  9169  php4  9172  isfinite2  9236  imafiOLD  9254  fundmfibi  9273  fiinfcl  9443  wofib  9487  r1limg  9723  r1pwcl  9799  cardmin2  9951  zornn0g  10456  mptct  10489  intgru  10766  supsrlem  11063  nzadd  12613  fnn0ind  12666  uztrn2  12852  nnwo  12908  irradd  12968  qbtwnxr  13197  xltnegi  13213  xaddnemnf  13233  xaddnepnf  13234  xaddcom  13237  xnegdi  13245  elioore  13373  uzsubsubfz1  13546  fzo1fzo0n0  13715  elfzonelfzo  13769  modsumfzodifsn  13951  leexp2  14178  faclbnd  14297  faclbnd3  14299  fi1uzind  14514  brfi1uzind  14515  opfi1uzind  14518  swrdccat3b  14747  dvdslelem  16334  divalglem1  16419  dvdsprime  16712  pcgcd  16905  cntri  19363  cntzsgrpcl  19365  efgsrel  19765  xrsdsreclb  21454  znf1o  21591  restuni  23210  stoig  23211  restperf  23232  resstps  23235  pnfnei  23268  mnfnei  23269  cnnei  23330  cmpsublem  23447  comppfsc  23580  tx1stc  23698  xkopt  23703  isfcls  24057  tgioo  24844  opnreen  24880  iscmet3  25343  dyaddisj  25646  limcmpt  25933  degltlem1  26120  ulmdvlem3  26453  lgsdi  27386  noreson  27712  divsclw  28276  cusgrres  29606  crctcshwlkn0lem4  29970  crctcshwlkn0lem5  29971  wwlksnred  30049  eupth2lem3lem4  30390  grpoidinvlem3  30666  ipasslem3  30993  spanuni  31704  5oalem3  31816  5oalem5  31818  mdslmd1lem2  32486  rnressnsn  32840  mptctf  32879  xaddeq0  32916  xnn0gt0  32932  ssdifidllem  33604  ssmxidllem  33622  ssmxidl  33623  ordtconnlem1  34182  esumcvg  34344  ldgenpisyslem1  34421  measdivcst  34482  measdivcstALTV  34483  probun  34677  fnrelpredd  35348  elwf  35354  r1omhf  35363  fineqvrep  35371  elmpps  35884  dfon2lem9  36100  funpartfun  36254  cgrxfr  36366  segcon2  36416  brsegle2  36420  seglecgr12im  36421  segletr  36425  nn0prpw  36644  bj-seex  37368  bj-axreprepsep  37521  bj-prmoore  37566  fvineqsneu  37866  lindsenlbs  38075  matunitlindflem2  38077  ptrecube  38080  poimirlem28  38108  ftc1anclem5  38157  ftc1anc  38161  exlimddvfi  38582  imadomfi  42580  readvrec  42932  nn0addcom  43045  nn0mulcom  43049  riccrng1  43100  ricdrng1  43107  mzpclall  43269  4an31  45035  cnrefiisplem  46364  iundjiun  46995  funbrafvb  47711  funopafvb  47712  afvco2  47731  dfatbrafv2b  47800  funbrafv22b  47805  funopafv2b  47806  sprsymrelfolem2  48060  uhgrimgrlim  48570  line2xlem  49336  itsclc0xyqsol  49351  f1mo  49435  catprs  49593  setrec2lem2  50276