Theorem syl2anb 285

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 278	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
5	1, 4	sylan2b 281	1 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sylancb  409  reupick3  3282  difprsnss  3570  trin2  4810  imadiflem  5079  fnun  5106  fco  5161  f1co  5212  foco  5227  f1oun  5257  f1oco  5260  eqfunfv  5386  ftpg  5465  issmo  6035  tfrlem5  6061  ener  6476  domtr  6482  unen  6513  xpdom2  6527  mapen  6542  pm54.43  6797  axpre-lttrn  7398  axpre-mulgt0  7401  zmulcl  8773  qaddcl  9089  qmulcl  9091  rpaddcl  9126  rpmulcl  9127  rpdivcl  9128  xrltnsym  9232  xrlttri3  9236  ge0addcl  9368  ge0mulcl  9369  expclzaplem  9944  expge0  9956  expge1  9957  hashfacen  10206  qredeu  11161  nn0gcdsq  11260