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  3422  difprsnss  3732  trin2  5022  imadiflem  5297  fnun  5324  fco  5383  f1co  5435  foco  5450  f1oun  5483  f1oco  5486  eqfunfv  5620  ftpg  5702  issmo  6291  tfrlem5  6317  ener  6781  domtr  6787  unen  6818  xpdom2  6833  mapen  6848  pm54.43  7191  axpre-lttrn  7885  axpre-mulgt0  7888  zmulcl  9308  qaddcl  9637  qmulcl  9639  rpaddcl  9679  rpmulcl  9680  rpdivcl  9681  xrltnsym  9795  xrlttri3  9799  ge0addcl  9983  ge0mulcl  9984  ge0xaddcl  9985  expclzaplem  10546  expge0  10558  expge1  10559  hashfacen  10818  qredeu  12099  nn0gcdsq  12202  mul4sq  12394  cnovex  13735  iscn2  13739  txuni  13802  txcn  13814  lgsne0  14478  mul2sq  14502