Theorem sylanb 593

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  syl2anb  610  anabsan  678  rmob  3836  sspsstr  4036  disjne  4407  ssexg  5280  rexopabb  5501  seex  5609  xpcan2  6168  tron  6385  fcof  6734  fssres  6749  funbrfvb  6939  funopfvb  6940  fvco  6984  fvimacnvi  7052  ffvresb  7127  funressn  7164  funresdfunsn  7195  fvtp2  7202  fvtp2g  7205  fnex  7224  funex  7226  ordsucss  7830  ordsucelsuc  7834  1st2nd  8051  1stconst  8114  2ndconst  8115  frxp  8141  imacosupp  8230  dftpos4  8266  tz7.48lemOLD  8455  nnmsucr  8638  nnmcan  8647  xpmapenlem  9167  php  9226  php4  9229  isfinite2  9294  fundmfibi  9329  fiinfcl  9499  wofib  9543  r1limg  9782  elwf  9846  r1pwcl  9865  setrec2lem2  9980  cardmin2  10084  zornn0g  10587  mptct  10626  intgru  10903  supsrlem  11200  nzadd  12748  fnn0ind  12802  uztrn2  12988  nnwo  13044  irradd  13105  qbtwnxr  13334  xltnegi  13350  xaddnemnf  13370  xaddnepnf  13371  xaddcom  13374  xnegdi  13382  elioore  13510  uzsubsubfz1  13685  fzo1fzo0n0  13854  elfzonelfzo  13908  modsumfzodifsn  14091  leexp2  14318  faclbnd  14438  faclbnd3  14440  fi1uzind  14656  brfi1uzind  14657  opfi1uzind  14660  swrdccat3b  14894  dvdslelem  16485  divalglem1  16570  dvdsprime  16868  pcgcd  17062  cntri  19552  cntzsgrpcl  19554  efgsrel  19954  ssdifidllem  21646  xrsdsreclb  21726  znf1o  21863  lindsenlbs  22163  matunitlindflem2  23001  restuni  23486  stoig  23487  restperf  23508  resstps  23511  pnfnei  23544  mnfnei  23545  cnnei  23606  cmpsublem  23723  comppfsc  23857  tx1stc  23975  xkopt  23980  isfcls  24334  tgioo  25121  opnreen  25157  iscmet3  25620  dyaddisj  25923  limcmpt  26209  degltlem1  26396  ulmdvlem3  26735  lgsdi  27667  noreson  28023  divsclw  28587  cusgrres  30035  crctcshwlkn0lem4  30408  crctcshwlkn0lem5  30409  wwlksnred  30487  eupth2lem3lem4  30838  grpoidinvlem3  31114  ipasslem3  31441  spanuni  32152  5oalem3  32264  5oalem5  32266  mdslmd1lem2  32934  rnressnsn  33319  mptctf  33356  xaddeq0  33392  xnn0gt0  33408  ssmxidllem  34045  ssmxidl  34046  ordtconnlem1  34603  esumcvg  34765  ldgenpisyslem1  34843  measdivcst  34904  measdivcstALTV  34905  probun  35098  fnrelpredd  35773  fineqvrep  35839  elmpps  36425  dfon2lem9  36646  funpartfun  36800  cgrxfr  36913  segcon2  36963  brsegle2  36967  seglecgr12im  36968  segletr  36972  nn0prpw  37204  mh-inf3f1  37422  bj-seex  37927  bj-axreprepsep  38084  bj-prmoore  38129  fvineqsneu  38428  ptrecube  38632  poimirlem28  38660  ftc1anclem5  38709  ftc1anc  38713  exlimddvfi  39148  imadomfi  43146  readvrec  43507  nn0addcom  43620  nn0mulcom  43624  riccrng1  43676  ricdrng1  43686  mzpclall  43832  4an31  45575  cnrefiisplem  46933  iundjiun  47564  funbrafvb  48320  funopafvb  48321  afvco2  48340  dfatbrafv2b  48409  funbrafv22b  48414  funopafv2b  48415  sprsymrelfolem2  48669  uhgrimgrlim  49179  line2xlem  49959  itsclc0xyqsol  49974  f1mo  50058  catprs  50219