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  3459  difprsnss  3773  trin2  5079  fundif  5323  imadiflem  5358  fnun  5387  fco  5447  f1co  5500  foco  5516  f1oun  5549  f1oco  5552  eqfunfv  5689  ftpg  5775  issmo  6381  tfrlem5  6407  ener  6878  domtr  6884  unen  6915  xpdom2  6933  mapen  6950  pm54.43  7305  axpre-lttrn  8004  axpre-mulgt0  8007  zmulcl  9433  qaddcl  9763  qmulcl  9765  rpaddcl  9806  rpmulcl  9807  rpdivcl  9808  xrltnsym  9922  xrlttri3  9926  ge0addcl  10110  ge0mulcl  10111  ge0xaddcl  10112  expclzaplem  10715  expge0  10727  expge1  10728  hashfacen  10988  qredeu  12463  nn0gcdsq  12566  mul4sq  12761  cnovex  14712  iscn2  14716  txuni  14779  txcn  14791  lgsne0  15559  mul2sq  15637