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  4482  tron  4529  fssres  5568  funbrfvb  5746  funopfvb  5747  fvelrnb  5753  fvco  5778  fvimacnvi  5826  ffvresb  5874  fcof  5897  funresdfunsnss  5921  fvtp2g  5927  fvtp2  5930  fnex  5940  funex  5943  1st2nd  6419  imacosuppfn  6512  dftpos4  6539  nnmsucr  6766  nnmcan  6797  xpmapenlem  7155  fundmfibi  7258  sup3exmid  9295  nzadd  9706  peano5uzti  9764  fnn0ind  9772  uztrn2  9955  irradd  10061  xltnegi  10253  xaddnemnf  10275  xaddnepnf  10276  xaddcom  10279  xnegdi  10286  elioore  10330  uzsubsubfz1  10469  fzo1fzo0n0  10611  elfzonelfzo  10664  qbtwnxr  10708  faclbnd  11200  faclbnd3  11202  swrdccat3b  11533  dvdsprime  12924  pcgcd  13136  cntri  14164  cntzsgrpcl  14166  znf1o  15094  restuni  15415  stoig  15416  cnnei  15475  tgioo  15797  divcnap  15808  ivthdich  15896  lgsdi  16378  bj-indind  17180