Theorem sylan2br 348

Description: A syllogism inference.

Hypotheses

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

Assertion

Ref	Expression
sylan2br	⊢ ((φ ∧ θ) → χ)

Proof of Theorem sylan2br

Step	Hyp	Ref	Expression
1		sylan.1	. 2 ⊢ ((φ ∧ ψ) → χ)
2		sylan2br.2	. . 3 ⊢ (ψ ↔ θ)
3	2	biimpr 134	. 2 ⊢ (θ → ψ)
4	1, 3	sylan2 346	1 ⊢ ((φ ∧ θ) → χ)

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196

This theorem is referenced by:  syl2anbr 351  po2nr 2135  tfindsg2 2403  imainss 2649  imadif 2714  fnop 2727  tfrlem2 2950  tz7.48-2 2995  aceq5 3563  ac6lem 3575  zornlem7 3609  suppsr 4016  supsrlem6 4024  supre 4054  uzind2 4604  axhis42 5049  hoco 5598

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org