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  rmob  3840  sspsstr  4060  disjne  4407  rexopabb  5476  seex  5583  xpcan2  6135  tron  6340  fcof  6685  fssres  6700  funbrfvb  6887  funopfvb  6888  fvco  6932  fvimacnvi  6997  ffvresb  7070  funressn  7104  funresdfunsn  7135  fvtp2  7142  fvtp2g  7145  fnex  7163  funex  7165  ordsucss  7760  ordsucelsuc  7764  1st2nd  7983  1stconst  8042  2ndconst  8043  frxp  8068  imacosupp  8151  dftpos4  8187  tz7.48lem  8372  nnmsucr  8553  nnmcan  8562  xpmapenlem  9072  php  9131  php4  9134  isfinite2  9198  imafiOLD  9216  fundmfibi  9236  fiinfcl  9406  wofib  9450  r1limg  9683  r1pwcl  9759  cardmin2  9911  zornn0g  10415  mptct  10448  intgru  10725  supsrlem  11022  nzadd  12539  fnn0ind  12591  uztrn2  12770  nnwo  12826  irradd  12886  qbtwnxr  13115  xltnegi  13131  xaddnemnf  13151  xaddnepnf  13152  xaddcom  13155  xnegdi  13163  elioore  13291  uzsubsubfz1  13463  fzo1fzo0n0  13631  elfzonelfzo  13685  modsumfzodifsn  13867  leexp2  14094  faclbnd  14213  faclbnd3  14215  fi1uzind  14430  brfi1uzind  14431  opfi1uzind  14434  swrdccat3b  14663  dvdslelem  16236  divalglem1  16321  dvdsprime  16614  pcgcd  16806  cntri  19261  cntzsgrpcl  19263  efgsrel  19663  xrsdsreclb  21368  znf1o  21506  restuni  23106  stoig  23107  restperf  23128  resstps  23131  pnfnei  23164  mnfnei  23165  cnnei  23226  cmpsublem  23343  comppfsc  23476  tx1stc  23594  xkopt  23599  isfcls  23953  tgioo  24740  opnreen  24776  iscmet3  25249  dyaddisj  25553  limcmpt  25840  degltlem1  26033  ulmdvlem3  26367  lgsdi  27301  noreson  27628  divsclw  28191  cusgrres  29522  crctcshwlkn0lem4  29886  crctcshwlkn0lem5  29887  wwlksnred  29965  eupth2lem3lem4  30306  grpoidinvlem3  30581  ipasslem3  30908  spanuni  31619  5oalem3  31731  5oalem5  31733  mdslmd1lem2  32401  rnressnsn  32756  mptctf  32795  xaddeq0  32833  xnn0gt0  32849  ssdifidllem  33537  ssmxidllem  33554  ssmxidl  33555  ordtconnlem1  34081  esumcvg  34243  ldgenpisyslem1  34320  measdivcst  34381  measdivcstALTV  34382  probun  34576  fnrelpredd  35247  elwf  35253  r1omhf  35262  fineqvrep  35270  elmpps  35767  dfon2lem9  35983  funpartfun  36137  cgrxfr  36249  segcon2  36299  brsegle2  36303  seglecgr12im  36304  segletr  36308  nn0prpw  36517  bj-seex  37123  bj-prmoore  37320  fvineqsneu  37616  lindsenlbs  37816  matunitlindflem2  37818  ptrecube  37821  poimirlem28  37849  ftc1anclem5  37898  ftc1anc  37902  exlimddvfi  38323  imadomfi  42256  readvrec  42617  nn0addcom  42717  nn0mulcom  42721  riccrng1  42776  ricdrng1  42783  mzpclall  42969  4an31  44739  cnrefiisplem  46073  iundjiun  46704  funbrafvb  47402  funopafvb  47403  afvco2  47422  dfatbrafv2b  47491  funbrafv22b  47496  funopafv2b  47497  sprsymrelfolem2  47739  uhgrimgrlim  48233  line2xlem  48999  itsclc0xyqsol  49014  f1mo  49098  catprs  49256  setrec2lem2  49939