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  846  reupick3  3449  difprsnss  3761  trin2  5062  imadiflem  5338  fnun  5367  fco  5426  f1co  5478  foco  5494  f1oun  5527  f1oco  5530  eqfunfv  5667  ftpg  5749  issmo  6355  tfrlem5  6381  ener  6847  domtr  6853  unen  6884  xpdom2  6899  mapen  6916  pm54.43  7269  axpre-lttrn  7968  axpre-mulgt0  7971  zmulcl  9396  qaddcl  9726  qmulcl  9728  rpaddcl  9769  rpmulcl  9770  rpdivcl  9771  xrltnsym  9885  xrlttri3  9889  ge0addcl  10073  ge0mulcl  10074  ge0xaddcl  10075  expclzaplem  10672  expge0  10684  expge1  10685  hashfacen  10945  qredeu  12290  nn0gcdsq  12393  mul4sq  12588  cnovex  14516  iscn2  14520  txuni  14583  txcn  14595  lgsne0  15363  mul2sq  15441