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  3856  sspsstr  4074  disjne  4421  rexopabb  5491  seex  5600  xpcan2  6153  tron  6358  fcof  6714  fssres  6729  funbrfvb  6917  funopfvb  6918  fvco  6962  fvimacnvi  7027  ffvresb  7100  funressn  7134  funresdfunsn  7166  fvtp2  7173  fvtp2g  7176  fnex  7194  funex  7196  ordsucss  7796  ordsucelsuc  7800  1st2nd  8021  1stconst  8082  2ndconst  8083  frxp  8108  imacosupp  8191  dftpos4  8227  tz7.48lem  8412  nnmsucr  8592  nnmcan  8601  xpmapenlem  9114  php  9177  php4  9180  isfinite2  9252  imafiOLD  9272  fundmfibi  9294  fiinfcl  9461  wofib  9505  r1limg  9731  r1pwcl  9807  cardmin2  9959  zornn0g  10465  mptct  10498  intgru  10774  supsrlem  11071  nzadd  12588  fnn0ind  12640  uztrn2  12819  nnwo  12879  irradd  12939  qbtwnxr  13167  xltnegi  13183  xaddnemnf  13203  xaddnepnf  13204  xaddcom  13207  xnegdi  13215  elioore  13343  uzsubsubfz1  13515  fzo1fzo0n0  13683  elfzonelfzo  13737  modsumfzodifsn  13916  leexp2  14143  faclbnd  14262  faclbnd3  14264  fi1uzind  14479  brfi1uzind  14480  opfi1uzind  14483  swrdccat3b  14712  dvdslelem  16286  divalglem1  16371  dvdsprime  16664  pcgcd  16856  cntri  19271  cntzsgrpcl  19273  efgsrel  19671  xrsdsreclb  21337  znf1o  21468  restuni  23056  stoig  23057  restperf  23078  resstps  23081  pnfnei  23114  mnfnei  23115  cnnei  23176  cmpsublem  23293  comppfsc  23426  tx1stc  23544  xkopt  23549  isfcls  23903  tgioo  24691  opnreen  24727  iscmet3  25200  dyaddisj  25504  limcmpt  25791  degltlem1  25984  ulmdvlem3  26318  lgsdi  27252  noreson  27579  divsclw  28105  cusgrres  29383  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  wwlksnred  29829  eupth2lem3lem4  30167  grpoidinvlem3  30442  ipasslem3  30769  spanuni  31480  5oalem3  31592  5oalem5  31594  mdslmd1lem2  32262  mptctf  32648  xaddeq0  32683  xnn0gt0  32699  ssdifidllem  33434  ssmxidllem  33451  ssmxidl  33452  ordtconnlem1  33921  esumcvg  34083  ldgenpisyslem1  34160  measdivcst  34221  measdivcstALTV  34222  probun  34417  fnrelpredd  35086  fineqvrep  35092  elmpps  35567  dfon2lem9  35786  funpartfun  35938  cgrxfr  36050  segcon2  36100  brsegle2  36104  seglecgr12im  36105  segletr  36109  nn0prpw  36318  bj-seex  36917  bj-prmoore  37110  fvineqsneu  37406  lindsenlbs  37616  matunitlindflem2  37618  ptrecube  37621  poimirlem28  37649  ftc1anclem5  37698  ftc1anc  37702  exlimddvfi  38123  imadomfi  41997  readvrec  42357  nn0addcom  42457  nn0mulcom  42461  riccrng1  42516  ricdrng1  42523  mzpclall  42722  4an31  44495  cnrefiisplem  45834  iundjiun  46465  funbrafvb  47161  funopafvb  47162  afvco2  47181  dfatbrafv2b  47250  funbrafv22b  47255  funopafv2b  47256  sprsymrelfolem2  47498  uhgrimgrlim  47990  line2xlem  48746  itsclc0xyqsol  48761  f1mo  48845  catprs  49004  setrec2lem2  49687