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  3836  sspsstr  4053  disjne  4400  rexopabb  5463  seex  5570  xpcan2  6119  tron  6324  fcof  6669  fssres  6684  funbrfvb  6870  funopfvb  6871  fvco  6915  fvimacnvi  6980  ffvresb  7053  funressn  7087  funresdfunsn  7118  fvtp2  7125  fvtp2g  7128  fnex  7146  funex  7148  ordsucss  7743  ordsucelsuc  7747  1st2nd  7966  1stconst  8025  2ndconst  8026  frxp  8051  imacosupp  8134  dftpos4  8170  tz7.48lem  8355  nnmsucr  8535  nnmcan  8544  xpmapenlem  9052  php  9111  php4  9114  isfinite2  9177  imafiOLD  9195  fundmfibi  9215  fiinfcl  9382  wofib  9426  r1limg  9659  r1pwcl  9735  cardmin2  9887  zornn0g  10391  mptct  10424  intgru  10700  supsrlem  10997  nzadd  12515  fnn0ind  12567  uztrn2  12746  nnwo  12806  irradd  12866  qbtwnxr  13094  xltnegi  13110  xaddnemnf  13130  xaddnepnf  13131  xaddcom  13134  xnegdi  13142  elioore  13270  uzsubsubfz1  13442  fzo1fzo0n0  13610  elfzonelfzo  13664  modsumfzodifsn  13846  leexp2  14073  faclbnd  14192  faclbnd3  14194  fi1uzind  14409  brfi1uzind  14410  opfi1uzind  14413  swrdccat3b  14642  dvdslelem  16215  divalglem1  16300  dvdsprime  16593  pcgcd  16785  cntri  19239  cntzsgrpcl  19241  efgsrel  19641  xrsdsreclb  21345  znf1o  21483  restuni  23072  stoig  23073  restperf  23094  resstps  23097  pnfnei  23130  mnfnei  23131  cnnei  23192  cmpsublem  23309  comppfsc  23442  tx1stc  23560  xkopt  23565  isfcls  23919  tgioo  24706  opnreen  24742  iscmet3  25215  dyaddisj  25519  limcmpt  25806  degltlem1  25999  ulmdvlem3  26333  lgsdi  27267  noreson  27594  divsclw  28129  cusgrres  29422  crctcshwlkn0lem4  29786  crctcshwlkn0lem5  29787  wwlksnred  29865  eupth2lem3lem4  30203  grpoidinvlem3  30478  ipasslem3  30805  spanuni  31516  5oalem3  31628  5oalem5  31630  mdslmd1lem2  32298  mptctf  32691  xaddeq0  32728  xnn0gt0  32744  ssdifidllem  33413  ssmxidllem  33430  ssmxidl  33431  ordtconnlem1  33929  esumcvg  34091  ldgenpisyslem1  34168  measdivcst  34229  measdivcstALTV  34230  probun  34424  fnrelpredd  35094  elwf  35100  r1omhf  35109  fineqvrep  35129  elmpps  35609  dfon2lem9  35825  funpartfun  35977  cgrxfr  36089  segcon2  36139  brsegle2  36143  seglecgr12im  36144  segletr  36148  nn0prpw  36357  bj-seex  36956  bj-prmoore  37149  fvineqsneu  37445  lindsenlbs  37655  matunitlindflem2  37657  ptrecube  37660  poimirlem28  37688  ftc1anclem5  37737  ftc1anc  37741  exlimddvfi  38162  imadomfi  42035  readvrec  42395  nn0addcom  42495  nn0mulcom  42499  riccrng1  42554  ricdrng1  42561  mzpclall  42760  4an31  44531  cnrefiisplem  45867  iundjiun  46498  funbrafvb  47187  funopafvb  47188  afvco2  47207  dfatbrafv2b  47276  funbrafv22b  47281  funopafv2b  47282  sprsymrelfolem2  47524  uhgrimgrlim  48018  line2xlem  48785  itsclc0xyqsol  48800  f1mo  48884  catprs  49043  setrec2lem2  49726