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  7271  axpre-lttrn  7970  axpre-mulgt0  7973  zmulcl  9398  qaddcl  9728  qmulcl  9730  rpaddcl  9771  rpmulcl  9772  rpdivcl  9773  xrltnsym  9887  xrlttri3  9891  ge0addcl  10075  ge0mulcl  10076  ge0xaddcl  10077  expclzaplem  10674  expge0  10686  expge1  10687  hashfacen  10947  qredeu  12292  nn0gcdsq  12395  mul4sq  12590  cnovex  14518  iscn2  14522  txuni  14585  txcn  14597  lgsne0  15365  mul2sq  15443