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  845  reupick3  3420  difprsnss  3730  trin2  5020  imadiflem  5295  fnun  5322  fco  5381  f1co  5433  foco  5448  f1oun  5481  f1oco  5484  eqfunfv  5618  ftpg  5700  issmo  6288  tfrlem5  6314  ener  6778  domtr  6784  unen  6815  xpdom2  6830  mapen  6845  pm54.43  7188  axpre-lttrn  7882  axpre-mulgt0  7885  zmulcl  9305  qaddcl  9634  qmulcl  9636  rpaddcl  9676  rpmulcl  9677  rpdivcl  9678  xrltnsym  9792  xrlttri3  9796  ge0addcl  9980  ge0mulcl  9981  ge0xaddcl  9982  expclzaplem  10543  expge0  10555  expge1  10556  hashfacen  10815  qredeu  12096  nn0gcdsq  12199  mul4sq  12391  cnovex  13666  iscn2  13670  txuni  13733  txcn  13745  lgsne0  14409  mul2sq  14433