Theorem syl2anb 287

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylancb  412  stdcndc  813  reupick3  3325  difprsnss  3622  trin2  4886  imadiflem  5158  fnun  5185  fco  5244  f1co  5296  foco  5311  f1oun  5341  f1oco  5344  eqfunfv  5475  ftpg  5556  issmo  6137  tfrlem5  6163  ener  6625  domtr  6631  unen  6662  xpdom2  6676  mapen  6691  pm54.43  6993  axpre-lttrn  7613  axpre-mulgt0  7616  zmulcl  9005  qaddcl  9323  qmulcl  9325  rpaddcl  9360  rpmulcl  9361  rpdivcl  9362  xrltnsym  9466  xrlttri3  9470  ge0addcl  9651  ge0mulcl  9652  ge0xaddcl  9653  expclzaplem  10204  expge0  10216  expge1  10217  hashfacen  10466  qredeu  11618  nn0gcdsq  11717  iscn2  12205  txuni  12268  txcn  12280