Theorem syl2anb 289

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 282	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2b 285	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylancb  415  stdcndc  835  reupick3  3402  difprsnss  3705  trin2  4989  imadiflem  5261  fnun  5288  fco  5347  f1co  5399  foco  5414  f1oun  5446  f1oco  5449  eqfunfv  5582  ftpg  5663  issmo  6247  tfrlem5  6273  ener  6736  domtr  6742  unen  6773  xpdom2  6788  mapen  6803  pm54.43  7137  axpre-lttrn  7816  axpre-mulgt0  7819  zmulcl  9235  qaddcl  9564  qmulcl  9566  rpaddcl  9604  rpmulcl  9605  rpdivcl  9606  xrltnsym  9720  xrlttri3  9724  ge0addcl  9908  ge0mulcl  9909  ge0xaddcl  9910  expclzaplem  10469  expge0  10481  expge1  10482  hashfacen  10735  qredeu  12008  nn0gcdsq  12109  cnovex  12737  iscn2  12741  txuni  12804  txcn  12816