Theorem sylanb 284

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  syl2anb  291  anabsan  575  2exeu  2170  eqtr2  2248  pm13.181  2482  rmob  3122  disjne  3545  seex  4425  tron  4472  fssres  5500  funbrfvb  5673  funopfvb  5674  fvelrnb  5680  fvco  5703  fvimacnvi  5748  ffvresb  5797  funresdfunsnss  5841  fvtp2g  5847  fvtp2  5850  fnex  5860  funex  5861  1st2nd  6325  dftpos4  6407  nnmsucr  6632  nnmcan  6663  xpmapenlem  7006  fundmfibi  7101  sup3exmid  9100  nzadd  9495  peano5uzti  9551  fnn0ind  9559  uztrn2  9736  irradd  9837  xltnegi  10027  xaddnemnf  10049  xaddnepnf  10050  xaddcom  10053  xnegdi  10060  elioore  10104  uzsubsubfz1  10240  fzo1fzo0n0  10379  elfzonelfzo  10431  qbtwnxr  10472  faclbnd  10958  faclbnd3  10960  swrdccat3b  11267  dvdsprime  12639  pcgcd  12847  znf1o  14609  restuni  14840  stoig  14841  cnnei  14900  tgioo  15222  divcnap  15233  ivthdich  15321  lgsdi  15710  bj-indind  16253