Theorem sylan2b 461

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)

Hypotheses

Ref	Expression
sylan2b.1	⊢ (φ ↔ χ)
sylan2b.2	⊢ ((ψ ∧ χ) → θ)

Assertion

Ref	Expression
sylan2b	⊢ ((ψ ∧ φ) → θ)

Proof of Theorem sylan2b

Step	Hyp	Ref	Expression
1		sylan2b.1	. . 3 ⊢ (φ ↔ χ)
2	1	biimpi 186	. 2 ⊢ (φ → χ)
3		sylan2b.2	. 2 ⊢ ((ψ ∧ χ) → θ)
4	2, 3	sylan2 460	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:  syl2anb  465  bm1.1  2338  eqtr3  2372  morex  3020  psssstr  3375  reuss2  3535  reupick  3539  reximdva0  3561  rabsneu  3795  reiota2  4368  nnsucelr  4428  nndisjeq  4429  prepeano4  4451  lefinlteq  4463  ltlefin  4468  ncfinraise  4481  sfindbl  4530  nulnnn  4556  xpcan  5057  fnfco  5237  fun11iun  5305  tz6.12-1  5344  fnressn  5438  fndmeng  6046