Theorem sylanb 583

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

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

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 399

This theorem is referenced by:  syl2anb  599  anabsan  663  eqtr2  2842  pm13.181  3099  rmob  3873  sspsstr  4081  disjne  4403  rexopabb  5414  seex  5517  xpcan2  6033  tron  6213  fssres  6543  funbrfvb  6719  funopfvb  6720  fvco  6758  fvimacnvi  6821  ffvresb  6887  funressn  6920  funresdfunsn  6950  fvtp2  6957  fvtp2g  6960  fnex  6979  funex  6981  ordsucss  7532  ordsucelsuc  7536  1st2nd  7737  1stconst  7794  2ndconst  7795  frxp  7819  imacosupp  7873  dftpos4  7910  tz7.48lem  8076  nnmsucr  8250  nnmcan  8259  xpmapenlem  8683  php  8700  php4  8703  isfinite2  8775  fundmfibi  8802  fiinfcl  8964  wofib  9008  r1limg  9199  r1pwcl  9275  cardmin2  9426  zornn0g  9926  mptct  9959  intgru  10235  supsrlem  10532  nzadd  12029  fnn0ind  12080  uztrn2  12261  nnwo  12312  irradd  12371  qbtwnxr  12592  xltnegi  12608  xaddnemnf  12628  xaddnepnf  12629  xaddcom  12632  xnegdi  12640  elioore  12767  uzsubsubfz1  12929  fzo1fzo0n0  13087  elfzonelfzo  13138  modsumfzodifsn  13311  leexp2  13534  faclbnd  13649  faclbnd3  13651  fi1uzind  13854  brfi1uzind  13855  opfi1uzind  13858  swrdccat3b  14101  dvdslelem  15658  divalglem1  15744  dvdsprime  16030  pcgcd  16213  cntri  18460  efgsrel  18859  xrsdsreclb  20591  znf1o  20697  restuni  21769  stoig  21770  restperf  21791  resstps  21794  pnfnei  21827  mnfnei  21828  cnnei  21889  cmpsublem  22006  comppfsc  22139  tx1stc  22257  xkopt  22262  isfcls  22616  tgioo  23403  opnreen  23438  iscmet3  23895  dyaddisj  24196  limcmpt  24480  degltlem1  24665  ulmdvlem3  24989  lgsdi  25909  cusgrres  27229  crctcshwlkn0lem4  27590  crctcshwlkn0lem5  27591  wwlksnred  27669  eupth2lem3lem4  28009  grpoidinvlem3  28282  ipasslem3  28609  spanuni  29320  5oalem3  29432  5oalem5  29434  mdslmd1lem2  30102  mptctf  30452  xaddeq0  30476  xnn0gt0  30493  ssmxidllem  30978  ssmxidl  30979  ordtconnlem1  31167  esumcvg  31345  ldgenpisyslem1  31422  measdivcst  31483  measdivcstALTV  31484  probun  31677  elmpps  32820  dfon2lem9  33036  noreson  33167  funpartfun  33404  cgrxfr  33516  segcon2  33566  brsegle2  33570  seglecgr12im  33571  segletr  33575  nn0prpw  33671  bj-seex  34241  bj-prmoore  34406  fvineqsneu  34691  lindsenlbs  34886  matunitlindflem2  34888  ptrecube  34891  poimirlem28  34919  ftc1anclem5  34970  ftc1anc  34974  exlimddvfi  35399  mzpclall  39322  4an31  40830  cnrefiisplem  42108  iundjiun  42741  funbrafvb  43354  funopafvb  43355  afvco2  43374  dfatbrafv2b  43443  funbrafv22b  43448  funopafv2b  43449  sprsymrelfolem2  43654  line2xlem  44739  itsclc0xyqsol  44754  setrec2lem2  44796