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  853  reupick3  3510  difprsnss  3837  trin2  5159  fundif  5405  imadiflem  5440  fnun  5469  fco  5532  f1co  5590  foco  5606  f1oun  5639  f1oco  5642  eqfunfv  5785  ftpg  5873  issmo  6532  tfrlem5  6558  ener  7032  domtr  7038  unen  7071  xpdom2  7095  mapen  7112  pm54.43  7500  axpre-lttrn  8215  axpre-mulgt0  8218  zmulcl  9651  qaddcl  9988  qmulcl  9990  rpaddcl  10031  rpmulcl  10032  rpdivcl  10033  xrltnsym  10148  xrlttri3  10152  ge0addcl  10336  ge0mulcl  10337  ge0xaddcl  10338  expclzaplem  10952  expge0  10964  expge1  10965  hashfacen  11236  qredeu  12822  nn0gcdsq  12925  mul4sq  13120  ballotfilem2  13175  cnovex  15190  iscn2  15194  txuni  15257  txcn  15269  lgsne0  16040  mul2sq  16118