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 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylancb  422  stdcndc  857  reupick3  3518  difprsnss  3853  trin2  5179  fundif  5425  imadiflem  5460  fnun  5489  fco  5552  f1co  5610  foco  5626  f1oun  5659  f1oco  5662  eqfunfv  5811  ftpg  5899  issmo  6559  tfrlem5  6585  ener  7066  domtr  7072  unen  7105  xpdom2  7129  mapen  7146  pm54.43  7536  axpre-lttrn  8251  axpre-mulgt0  8254  zmulcl  9700  qaddcl  10037  qmulcl  10039  rpaddcl  10080  rpmulcl  10081  rpdivcl  10082  xrltnsym  10197  xrlttri3  10201  ge0addcl  10385  ge0mulcl  10386  ge0xaddcl  10387  expclzaplem  11002  expge0  11014  expge1  11015  hashfacen  11286  qredeu  12877  nn0gcdsq  12980  mul4sq  13175  ballotfilem2  13230  cnovex  15299  iscn2  15303  txuni  15366  txcn  15378  lgsne0  16169  mul2sq  16247