sylnibr - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > sylnibr		GIF version

Theorem sylnibr 296

Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)

**Hypotheses**
Ref	Expression
sylnibr.1	⊢ (φ → ¬ ψ)
sylnibr.2	⊢ (χ ↔ ψ)

**Assertion**
Ref	Expression
sylnibr	⊢ (φ → ¬ χ)

**Proof of Theorem sylnibr**
Step	Hyp	Ref	Expression
1		sylnibr.1	. 2 ⊢ (φ → ¬ ψ)
2		sylnibr.2	. . 3 ⊢ (χ ↔ ψ)
3	2	bicomi 193	. 2 ⊢ (ψ ↔ χ)
4	1, 3	sylnib 295	1 ⊢ (φ → ¬ χ)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 176

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

This theorem depends on definitions: df-bi 177

This theorem is referenced by: ncfinraise 4481 tfinltfin 4501 sfindbl 4530 tfinnn 4534 vfinncvntsp 4549 nnc3n3p1 6278 nnc3n3p2 6279 nnc3p1n3p2 6280 nchoicelem2 6290

W3C validator