baib - New Foundations Explorer

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

Theorem baib 871

Description: Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)

**Hypothesis**
Ref	Expression
baib.1	⊢ (φ ↔ (ψ ∧ χ))

**Assertion**
Ref	Expression
baib	⊢ (ψ → (φ ↔ χ))

**Proof of Theorem baib**
Step	Hyp	Ref	Expression
1		ibar 490	. 2 ⊢ (ψ → (χ ↔ (ψ ∧ χ)))
2		baib.1	. 2 ⊢ (φ ↔ (ψ ∧ χ))
3	1, 2	syl6rbbr 255	1 ⊢ (ψ → (φ ↔ χ))

Colors of variables: wff setvar class

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

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 df-an 360

This theorem is referenced by: baibr 872 rbaib 873 ceqsrexbv 2973 elrab3 2995 dfpss3 3355 rabsn 3790 elrint2 3968 fnres 5199 fvmpti 5699