Theorem sylanb 592

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  syl2anb  609  anabsan  677  rmob  3844  sspsstr  4064  disjne  4416  ssexg  5291  rexopabb  5514  seex  5622  xpcan2  6177  tron  6385  fcof  6731  fssres  6746  funbrfvb  6936  funopfvb  6937  fvco  6981  fvimacnvi  7049  ffvresb  7123  funressn  7158  funresdfunsn  7189  fvtp2  7196  fvtp2g  7199  fnex  7217  funex  7219  ordsucss  7815  ordsucelsuc  7819  1st2nd  8037  1stconst  8096  2ndconst  8097  frxp  8123  imacosupp  8206  dftpos4  8242  tz7.48lem  8429  nnmsucr  8612  nnmcan  8621  xpmapenlem  9133  php  9192  php4  9195  isfinite2  9259  fundmfibi  9294  fiinfcl  9464  wofib  9508  r1limg  9744  r1pwcl  9820  cardmin2  9986  zornn0g  10490  mptct  10523  intgru  10800  supsrlem  11097  nzadd  12643  fnn0ind  12696  uztrn2  12882  nnwo  12938  irradd  12998  qbtwnxr  13227  xltnegi  13243  xaddnemnf  13263  xaddnepnf  13264  xaddcom  13267  xnegdi  13275  elioore  13403  uzsubsubfz1  13577  fzo1fzo0n0  13746  elfzonelfzo  13800  modsumfzodifsn  13982  leexp2  14209  faclbnd  14328  faclbnd3  14330  fi1uzind  14546  brfi1uzind  14547  opfi1uzind  14550  swrdccat3b  14779  dvdslelem  16368  divalglem1  16453  dvdsprime  16746  pcgcd  16939  cntri  19403  cntzsgrpcl  19405  efgsrel  19805  ssdifidllem  21465  xrsdsreclb  21545  znf1o  21682  restuni  23300  stoig  23301  restperf  23322  resstps  23325  pnfnei  23358  mnfnei  23359  cnnei  23420  cmpsublem  23537  comppfsc  23670  tx1stc  23788  xkopt  23793  isfcls  24147  tgioo  24934  opnreen  24970  iscmet3  25433  dyaddisj  25736  limcmpt  26023  degltlem1  26210  ulmdvlem3  26546  lgsdi  27479  noreson  27805  divsclw  28369  cusgrres  29779  crctcshwlkn0lem4  30143  crctcshwlkn0lem5  30144  wwlksnred  30222  eupth2lem3lem4  30563  grpoidinvlem3  30839  ipasslem3  31166  spanuni  31877  5oalem3  31989  5oalem5  31991  mdslmd1lem2  32659  rnressnsn  33003  mptctf  33042  xaddeq0  33079  xnn0gt0  33095  ssmxidllem  33737  ssmxidl  33738  ordtconnlem1  34295  esumcvg  34457  ldgenpisyslem1  34534  measdivcst  34595  measdivcstALTV  34596  probun  34790  fnrelpredd  35463  elwf  35471  r1omhf  35481  fineqvrep  35508  elmpps  36046  dfon2lem9  36262  funpartfun  36416  cgrxfr  36528  segcon2  36578  brsegle2  36582  seglecgr12im  36583  segletr  36587  nn0prpw  36815  bj-seex  37538  bj-axreprepsep  37693  bj-prmoore  37738  fvineqsneu  38038  lindsenlbs  38247  matunitlindflem2  38249  ptrecube  38252  poimirlem28  38280  ftc1anclem5  38329  ftc1anc  38333  exlimddvfi  38752  imadomfi  42750  readvrec  43104  nn0addcom  43217  nn0mulcom  43221  riccrng1  43272  ricdrng1  43279  mzpclall  43441  4an31  45190  cnrefiisplem  46526  iundjiun  47157  funbrafvb  47876  funopafvb  47877  afvco2  47896  dfatbrafv2b  47965  funbrafv22b  47970  funopafv2b  47971  sprsymrelfolem2  48225  uhgrimgrlim  48735  line2xlem  49516  itsclc0xyqsol  49531  f1mo  49614  catprs  49772  setrec2lem2  50455