Theorem syl2anb 465

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 458	. 2 ⊢ ((φ ∧ χ) → θ)
5	1, 4	sylan2b 461	1 ⊢ ((φ ∧ τ) → θ)

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  sylancb  646  2eu6  2289  reupick3  3540  difprsnss  3846  ncfinraise  4481  ncfinlower  4483  sfinltfin  4535  fnun  5189  f1oun  5304  eqfunfv  5397  swapf1o  5511  fnfullfunlem2  5857  fvfullfunlem3  5863  xpassen  6057  enprmaplem3  6078  ncaddccl  6144  peano4nc  6150  cenc  6181