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  2118  eqtr2  2196  pm13.181  2429  rmob  3056  disjne  3477  seex  4336  tron  4383  fssres  5392  funbrfvb  5559  funopfvb  5560  fvelrnb  5564  fvco  5587  fvimacnvi  5631  ffvresb  5680  funresdfunsnss  5720  fvtp2g  5726  fvtp2  5729  fnex  5739  funex  5740  1st2nd  6182  dftpos4  6264  nnmsucr  6489  nnmcan  6520  xpmapenlem  6849  fundmfibi  6938  sup3exmid  8914  nzadd  9305  peano5uzti  9361  fnn0ind  9369  uztrn2  9545  irradd  9646  xltnegi  9835  xaddnemnf  9857  xaddnepnf  9858  xaddcom  9861  xnegdi  9868  elioore  9912  uzsubsubfz1  10048  fzo1fzo0n0  10183  elfzonelfzo  10230  qbtwnxr  10258  faclbnd  10721  faclbnd3  10723  dvdsprime  12122  pcgcd  12328  restuni  13675  stoig  13676  cnnei  13735  tgioo  14049  divcnap  14058  lgsdi  14441  bj-indind  14687