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  2147  eqtr2  2225  pm13.181  2459  rmob  3095  disjne  3518  seex  4390  tron  4437  fssres  5463  funbrfvb  5634  funopfvb  5635  fvelrnb  5639  fvco  5662  fvimacnvi  5707  ffvresb  5756  funresdfunsnss  5800  fvtp2g  5806  fvtp2  5809  fnex  5819  funex  5820  1st2nd  6280  dftpos4  6362  nnmsucr  6587  nnmcan  6618  xpmapenlem  6961  fundmfibi  7055  sup3exmid  9050  nzadd  9445  peano5uzti  9501  fnn0ind  9509  uztrn2  9686  irradd  9787  xltnegi  9977  xaddnemnf  9999  xaddnepnf  10000  xaddcom  10003  xnegdi  10010  elioore  10054  uzsubsubfz1  10190  fzo1fzo0n0  10329  elfzonelfzo  10381  qbtwnxr  10422  faclbnd  10908  faclbnd3  10910  dvdsprime  12519  pcgcd  12727  znf1o  14488  restuni  14719  stoig  14720  cnnei  14779  tgioo  15101  divcnap  15112  ivthdich  15200  lgsdi  15589  bj-indind  16006