Theorem syl2anb 291

Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)

Hypotheses

Ref	Expression
syl2anb.1	⊢ (𝜑 ↔ 𝜓)
syl2anb.2	⊢ (𝜏 ↔ 𝜒)
syl2anb.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syl2anb	⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Proof of Theorem syl2anb

Step	Hyp	Ref	Expression
1		syl2anb.2	. 2 ⊢ (𝜏 ↔ 𝜒)
2		syl2anb.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		syl2anb.3	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	sylanb 284	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2b 287	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:  sylancb  418  stdcndc  847  reupick3  3462  difprsnss  3777  trin2  5088  fundif  5332  imadiflem  5367  fnun  5396  fco  5456  f1co  5510  foco  5526  f1oun  5559  f1oco  5562  eqfunfv  5700  ftpg  5786  issmo  6392  tfrlem5  6418  ener  6889  domtr  6895  unen  6927  xpdom2  6946  mapen  6963  pm54.43  7319  axpre-lttrn  8027  axpre-mulgt0  8030  zmulcl  9456  qaddcl  9786  qmulcl  9788  rpaddcl  9829  rpmulcl  9830  rpdivcl  9831  xrltnsym  9945  xrlttri3  9949  ge0addcl  10133  ge0mulcl  10134  ge0xaddcl  10135  expclzaplem  10740  expge0  10752  expge1  10753  hashfacen  11013  qredeu  12504  nn0gcdsq  12607  mul4sq  12802  cnovex  14753  iscn2  14757  txuni  14820  txcn  14832  lgsne0  15600  mul2sq  15678