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  2137  eqtr2  2215  pm13.181  2449  rmob  3082  disjne  3505  seex  4371  tron  4418  fssres  5436  funbrfvb  5606  funopfvb  5607  fvelrnb  5611  fvco  5634  fvimacnvi  5679  ffvresb  5728  funresdfunsnss  5768  fvtp2g  5774  fvtp2  5777  fnex  5787  funex  5788  1st2nd  6248  dftpos4  6330  nnmsucr  6555  nnmcan  6586  xpmapenlem  6919  fundmfibi  7013  sup3exmid  9003  nzadd  9397  peano5uzti  9453  fnn0ind  9461  uztrn2  9638  irradd  9739  xltnegi  9929  xaddnemnf  9951  xaddnepnf  9952  xaddcom  9955  xnegdi  9962  elioore  10006  uzsubsubfz1  10142  fzo1fzo0n0  10278  elfzonelfzo  10325  qbtwnxr  10366  faclbnd  10852  faclbnd3  10854  dvdsprime  12317  pcgcd  12525  znf1o  14285  restuni  14516  stoig  14517  cnnei  14576  tgioo  14898  divcnap  14909  ivthdich  14997  lgsdi  15386  bj-indind  15686