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  3123  disjne  3546  seex  4430  tron  4477  fssres  5509  funbrfvb  5682  funopfvb  5683  fvelrnb  5689  fvco  5712  fvimacnvi  5757  ffvresb  5806  fcof  5828  funresdfunsnss  5852  fvtp2g  5858  fvtp2  5861  fnex  5871  funex  5872  1st2nd  6339  dftpos4  6424  nnmsucr  6651  nnmcan  6682  xpmapenlem  7030  fundmfibi  7128  sup3exmid  9127  nzadd  9522  peano5uzti  9578  fnn0ind  9586  uztrn2  9764  irradd  9870  xltnegi  10060  xaddnemnf  10082  xaddnepnf  10083  xaddcom  10086  xnegdi  10093  elioore  10137  uzsubsubfz1  10273  fzo1fzo0n0  10412  elfzonelfzo  10465  qbtwnxr  10507  faclbnd  10993  faclbnd3  10995  swrdccat3b  11311  dvdsprime  12684  pcgcd  12892  znf1o  14655  restuni  14886  stoig  14887  cnnei  14946  tgioo  15268  divcnap  15279  ivthdich  15367  lgsdi  15756  bj-indind  16463