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  2170  eqtr2  2248  pm13.181  2482  rmob  3122  disjne  3545  seex  4426  tron  4473  fssres  5503  funbrfvb  5676  funopfvb  5677  fvelrnb  5683  fvco  5706  fvimacnvi  5751  ffvresb  5800  fcof  5822  funresdfunsnss  5846  fvtp2g  5852  fvtp2  5855  fnex  5865  funex  5866  1st2nd  6333  dftpos4  6415  nnmsucr  6642  nnmcan  6673  xpmapenlem  7018  fundmfibi  7116  sup3exmid  9115  nzadd  9510  peano5uzti  9566  fnn0ind  9574  uztrn2  9752  irradd  9853  xltnegi  10043  xaddnemnf  10065  xaddnepnf  10066  xaddcom  10069  xnegdi  10076  elioore  10120  uzsubsubfz1  10256  fzo1fzo0n0  10395  elfzonelfzo  10448  qbtwnxr  10489  faclbnd  10975  faclbnd3  10977  swrdccat3b  11287  dvdsprime  12659  pcgcd  12867  znf1o  14630  restuni  14861  stoig  14862  cnnei  14921  tgioo  15243  divcnap  15254  ivthdich  15342  lgsdi  15731  bj-indind  16350