Theorem sylanb 278

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  syl2anb  285  anabsan  539  2exeu  2033  eqtr2  2099  pm13.181  2327  rmob  2906  disjne  3297  seex  4090  tron  4137  fssres  5086  funbrfvb  5237  funopfvb  5238  fvelrnb  5242  fvco  5264  fvimacnvi  5302  ffvresb  5349  fvtp2g  5391  fvtp2  5394  fnex  5404  funex  5405  1st2nd  5827  dftpos4  5901  nnmsucr  6090  nnmcan  6115  fundmfibi  6390  nzadd  8403  peano5uzti  8455  fnn0ind  8463  uztrn2  8636  irradd  8731  xltnegi  8902  elioore  8935  uzsubsubfz1  9067  fzo1fzo0n0  9192  elfzonelfzo  9239  qbtwnxr  9266  faclbnd  9668  faclbnd3  9670  dvdsprime  10504  bj-indind  10727