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  2145  eqtr2  2223  pm13.181  2457  rmob  3090  disjne  3513  seex  4380  tron  4427  fssres  5445  funbrfvb  5615  funopfvb  5616  fvelrnb  5620  fvco  5643  fvimacnvi  5688  ffvresb  5737  funresdfunsnss  5777  fvtp2g  5783  fvtp2  5786  fnex  5796  funex  5797  1st2nd  6257  dftpos4  6339  nnmsucr  6564  nnmcan  6595  xpmapenlem  6928  fundmfibi  7022  sup3exmid  9012  nzadd  9407  peano5uzti  9463  fnn0ind  9471  uztrn2  9648  irradd  9749  xltnegi  9939  xaddnemnf  9961  xaddnepnf  9962  xaddcom  9965  xnegdi  9972  elioore  10016  uzsubsubfz1  10152  fzo1fzo0n0  10288  elfzonelfzo  10340  qbtwnxr  10381  faclbnd  10867  faclbnd3  10869  dvdsprime  12363  pcgcd  12571  znf1o  14331  restuni  14562  stoig  14563  cnnei  14622  tgioo  14944  divcnap  14955  ivthdich  15043  lgsdi  15432  bj-indind  15732