ifpnannanb

Description: Factor conditional logic operator over nand in terms 2 and 3. (Contributed by RP, 21-Apr-2020)

		Ref	Expression
	Assertion	ifpnannanb	$⊢ if- (φ, (ψ ⊼ χ), (θ ⊼ τ)) \leftrightarrow (if- (φ, ψ, θ) ⊼ if- (φ, χ, τ))$

Step	Hyp	Ref	Expression
1		df-nan	$⊢ (ψ ⊼ χ) \leftrightarrow \neg (ψ \land χ)$
2		df-nan	$⊢ (θ ⊼ τ) \leftrightarrow \neg (θ \land τ)$
3		ifpbi23	$⊢ (((ψ ⊼ χ) \leftrightarrow \neg (ψ \land χ)) \land ((θ ⊼ τ) \leftrightarrow \neg (θ \land τ))) \to (if- (φ, (ψ ⊼ χ), (θ ⊼ τ)) \leftrightarrow if- (φ, \neg (ψ \land χ), \neg (θ \land τ)))$
4	1 2 3	mp2an	$⊢ if- (φ, (ψ ⊼ χ), (θ ⊼ τ)) \leftrightarrow if- (φ, \neg (ψ \land χ), \neg (θ \land τ))$
5		ifpananb	$⊢ if- (φ, (ψ \land χ), (θ \land τ)) \leftrightarrow (if- (φ, ψ, θ) \land if- (φ, χ, τ))$
6	5	notbii	$⊢ \neg if- (φ, (ψ \land χ), (θ \land τ)) \leftrightarrow \neg (if- (φ, ψ, θ) \land if- (φ, χ, τ))$
7		ifpnotnotb	$⊢ if- (φ, \neg (ψ \land χ), \neg (θ \land τ)) \leftrightarrow \neg if- (φ, (ψ \land χ), (θ \land τ))$
8		df-nan	$⊢ (if- (φ, ψ, θ) ⊼ if- (φ, χ, τ)) \leftrightarrow \neg (if- (φ, ψ, θ) \land if- (φ, χ, τ))$
9	6 7 8	3bitr4i	$⊢ if- (φ, \neg (ψ \land χ), \neg (θ \land τ)) \leftrightarrow (if- (φ, ψ, θ) ⊼ if- (φ, χ, τ))$
10	4 9	bitri	$⊢ if- (φ, (ψ ⊼ χ), (θ ⊼ τ)) \leftrightarrow (if- (φ, ψ, θ) ⊼ if- (φ, χ, τ))$

Metamath Proof Explorer