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 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  syl2anb  291  anabsan  581  2exeu  2179  eqtr2  2257  pm13.181  2502  rmob  3145  disjne  3578  seex  4480  tron  4527  fssres  5565  funbrfvb  5743  funopfvb  5744  fvelrnb  5750  fvco  5775  fvimacnvi  5823  ffvresb  5871  fcof  5894  funresdfunsnss  5918  fvtp2g  5924  fvtp2  5927  fnex  5937  funex  5940  1st2nd  6415  imacosuppfn  6508  dftpos4  6534  nnmsucr  6761  nnmcan  6792  xpmapenlem  7149  fundmfibi  7252  sup3exmid  9289  nzadd  9701  peano5uzti  9758  fnn0ind  9766  uztrn2  9949  irradd  10055  xltnegi  10247  xaddnemnf  10269  xaddnepnf  10270  xaddcom  10273  xnegdi  10280  elioore  10324  uzsubsubfz1  10463  fzo1fzo0n0  10605  elfzonelfzo  10658  qbtwnxr  10702  faclbnd  11193  faclbnd3  11195  swrdccat3b  11526  dvdsprime  12916  pcgcd  13128  znf1o  15035  restuni  15322  stoig  15323  cnnei  15382  tgioo  15704  divcnap  15715  ivthdich  15803  lgsdi  16254  bj-indind  17056