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  850  reupick3  3490  difprsnss  3809  trin2  5126  fundif  5371  imadiflem  5406  fnun  5435  fco  5497  f1co  5551  foco  5567  f1oun  5600  f1oco  5603  eqfunfv  5745  ftpg  5833  issmo  6449  tfrlem5  6475  ener  6948  domtr  6954  unen  6986  xpdom2  7010  mapen  7027  pm54.43  7389  axpre-lttrn  8097  axpre-mulgt0  8100  zmulcl  9526  qaddcl  9862  qmulcl  9864  rpaddcl  9905  rpmulcl  9906  rpdivcl  9907  xrltnsym  10021  xrlttri3  10025  ge0addcl  10209  ge0mulcl  10210  ge0xaddcl  10211  expclzaplem  10818  expge0  10830  expge1  10831  hashfacen  11093  qredeu  12662  nn0gcdsq  12765  mul4sq  12960  cnovex  14913  iscn2  14917  txuni  14980  txcn  14992  lgsne0  15760  mul2sq  15838