Theorem sylanbr 581

Description: A syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses

Ref	Expression
sylanbr.1	⊢ (𝜓 ↔ 𝜑)
sylanbr.2	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
sylanbr	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem sylanbr

Step	Hyp	Ref	Expression
1		sylanbr.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	biimpri 227	. 2 ⊢ (𝜑 → 𝜓)
3		sylanbr.2	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylan 579	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  syl2anbr  598  funfv  6837  2mpo0  7496  tfrlem7  8185  omword  8363  isinf  8965  fsuppunbi  9079  axdc3lem2  10138  supsrlem  10798  expclzlem  13734  expgt0  13744  expge0  13747  expge1  13748  swrdnd2  14296  resqrex  14890  rplpwr  16195  4sqlem19  16592  gexcl3  19107  thlle  20814  decpmataa0  21825  neindisj  22176  ptcmplem5  23115  tsmsxplem1  23212  tsmsxplem2  23213  elovolmr  24545  itgsubst  25118  logeftb  25644  logbchbase  25826  legov  26850  unopbd  30278  nmcoplb  30293  nmcfnlb  30317  nmopcoi  30358  iocinif  31004  voliune  32097  signstfvneq0  32451  lfuhgr3  32981  nosupbnd1lem5  33842  noinfbnd1lem5  33857  f1omptsnlem  35434  unccur  35687  matunitlindflem2  35701  stoweidlem15  43446  hoiqssbllem3  44052  vonioo  44110  vonicc  44113  gboge9  45104  catprs  46180