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  3249  difprsnss  3524  trin2  4736  imadiflem  4998  fnun  5025  fco  5076  f1co  5121  foco  5136  f1oun  5166  f1oco  5169  eqfunfv  5291  ftpg  5368  issmo  5926  tfrlem5  5953  ener  6282  domtr  6288  unen  6316  xpdom2  6328  pm54.43  6459  axpre-lttrn  7050  axpre-mulgt0  7053  zmulcl  8404  qaddcl  8720  qmulcl  8722  rpaddcl  8757  rpmulcl  8758  rpdivcl  8759  xrltnsym  8868  xrlttri3  8872  ge0addcl  9004  ge0mulcl  9005  serige0  9473  expclzaplem  9500  expge0  9512  expge1  9513  qredeu  10479