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  3055  disjne  3476  seex  4335  tron  4382  fssres  5391  funbrfvb  5558  funopfvb  5559  fvelrnb  5563  fvco  5586  fvimacnvi  5630  ffvresb  5679  funresdfunsnss  5719  fvtp2g  5725  fvtp2  5728  fnex  5738  funex  5739  1st2nd  6181  dftpos4  6263  nnmsucr  6488  nnmcan  6519  xpmapenlem  6848  fundmfibi  6937  sup3exmid  8913  nzadd  9304  peano5uzti  9360  fnn0ind  9368  uztrn2  9544  irradd  9645  xltnegi  9834  xaddnemnf  9856  xaddnepnf  9857  xaddcom  9860  xnegdi  9867  elioore  9911  uzsubsubfz1  10047  fzo1fzo0n0  10182  elfzonelfzo  10229  qbtwnxr  10257  faclbnd  10720  faclbnd3  10722  dvdsprime  12121  pcgcd  12327  restuni  13642  stoig  13643  cnnei  13702  tgioo  14016  divcnap  14025  lgsdi  14408  bj-indind  14654