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  577  2exeu  2173  eqtr2  2251  pm13.181  2494  rmob  3136  disjne  3562  seex  4456  tron  4503  fssres  5540  funbrfvb  5717  funopfvb  5718  fvelrnb  5724  fvco  5747  fvimacnvi  5792  ffvresb  5840  fcof  5863  funresdfunsnss  5887  fvtp2g  5893  fvtp2  5896  fnex  5906  funex  5909  1st2nd  6375  imacosuppfn  6468  dftpos4  6494  nnmsucr  6721  nnmcan  6752  xpmapenlem  7102  fundmfibi  7205  sup3exmid  9231  nzadd  9630  peano5uzti  9686  fnn0ind  9694  uztrn2  9872  irradd  9978  xltnegi  10168  xaddnemnf  10190  xaddnepnf  10191  xaddcom  10194  xnegdi  10201  elioore  10245  uzsubsubfz1  10382  fzo1fzo0n0  10522  elfzonelfzo  10575  qbtwnxr  10617  faclbnd  11103  faclbnd3  11105  swrdccat3b  11432  dvdsprime  12819  pcgcd  13027  znf1o  14799  restuni  15037  stoig  15038  cnnei  15097  tgioo  15419  divcnap  15430  ivthdich  15518  lgsdi  15910  bj-indind  16702