Theorem sylanb 282

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  syl2anb  289  anabsan  570  2exeu  2111  eqtr2  2189  pm13.181  2422  rmob  3047  disjne  3467  seex  4318  tron  4365  fssres  5371  funbrfvb  5537  funopfvb  5538  fvelrnb  5542  fvco  5564  fvimacnvi  5607  ffvresb  5656  funresdfunsnss  5696  fvtp2g  5702  fvtp2  5705  fnex  5715  funex  5716  1st2nd  6157  dftpos4  6239  nnmsucr  6464  nnmcan  6495  xpmapenlem  6823  fundmfibi  6912  sup3exmid  8860  nzadd  9251  peano5uzti  9307  fnn0ind  9315  uztrn2  9491  irradd  9592  xltnegi  9779  xaddnemnf  9801  xaddnepnf  9802  xaddcom  9805  xnegdi  9812  elioore  9856  uzsubsubfz1  9991  fzo1fzo0n0  10126  elfzonelfzo  10173  qbtwnxr  10201  faclbnd  10662  faclbnd3  10664  dvdsprime  12063  pcgcd  12269  restuni  12887  stoig  12888  cnnei  12947  tgioo  13261  divcnap  13270  lgsdi  13653  bj-indind  13889