ifpimim

		Ref	Expression
	Assertion	ifpimim	$⊢ if- (φ, (ψ \to χ), (θ \to τ)) \to (if- (φ, ψ, θ) \to if- (φ, χ, τ))$

Proof

Step	Hyp	Ref	Expression
1		pm2.521	$⊢ \neg (\neg φ \to φ) \to (φ \to \neg φ)$
2	1	orim1i	$⊢ (\neg (\neg φ \to φ) \lor (ψ \to χ)) \to ((φ \to \neg φ) \lor (ψ \to χ))$
3	2	adantr	$⊢ ((\neg (\neg φ \to φ) \lor (ψ \to χ)) \land ((\neg φ \to φ) \lor (θ \to τ))) \to ((φ \to \neg φ) \lor (ψ \to χ))$
4		id	$⊢ φ \to φ$
5	4	orci	$⊢ ((φ \to φ) \lor (θ \to χ))$
6	5	a1i	$⊢ ((\neg (\neg φ \to φ) \lor (ψ \to χ)) \land ((\neg φ \to φ) \lor (θ \to τ))) \to ((φ \to φ) \lor (θ \to χ))$
7	3 6	jca	$⊢ ((\neg (\neg φ \to φ) \lor (ψ \to χ)) \land ((\neg φ \to φ) \lor (θ \to τ))) \to (((φ \to \neg φ) \lor (ψ \to χ)) \land ((φ \to φ) \lor (θ \to χ)))$
8	4	orci	$⊢ ((φ \to φ) \lor (ψ \to τ))$
9	8	a1i	$⊢ ((\neg (\neg φ \to φ) \lor (ψ \to χ)) \land ((\neg φ \to φ) \lor (θ \to τ))) \to ((φ \to φ) \lor (ψ \to τ))$
10		simpr	$⊢ ((\neg (\neg φ \to φ) \lor (ψ \to χ)) \land ((\neg φ \to φ) \lor (θ \to τ))) \to ((\neg φ \to φ) \lor (θ \to τ))$
11	9 10	jca	$⊢ ((\neg (\neg φ \to φ) \lor (ψ \to χ)) \land ((\neg φ \to φ) \lor (θ \to τ))) \to (((φ \to φ) \lor (ψ \to τ)) \land ((\neg φ \to φ) \lor (θ \to τ)))$
12	7 11	jca	$⊢ ((\neg (\neg φ \to φ) \lor (ψ \to χ)) \land ((\neg φ \to φ) \lor (θ \to τ))) \to ((((φ \to \neg φ) \lor (ψ \to χ)) \land ((φ \to φ) \lor (θ \to χ))) \land (((φ \to φ) \lor (ψ \to τ)) \land ((\neg φ \to φ) \lor (θ \to τ))))$
13		pm4.81	$⊢ (\neg φ \to φ) \leftrightarrow φ$
14	13	bicomi	$⊢ φ \leftrightarrow (\neg φ \to φ)$
15		ifpbi1	$⊢ (φ \leftrightarrow (\neg φ \to φ)) \to (if- (φ, (ψ \to χ), (θ \to τ)) \leftrightarrow if- ((\neg φ \to φ), (ψ \to χ), (θ \to τ)))$
16	14 15	ax-mp	$⊢ if- (φ, (ψ \to χ), (θ \to τ)) \leftrightarrow if- ((\neg φ \to φ), (ψ \to χ), (θ \to τ))$
17		dfifp4	$⊢ if- ((\neg φ \to φ), (ψ \to χ), (θ \to τ)) \leftrightarrow ((\neg (\neg φ \to φ) \lor (ψ \to χ)) \land ((\neg φ \to φ) \lor (θ \to τ)))$
18	16 17	bitri	$⊢ if- (φ, (ψ \to χ), (θ \to τ)) \leftrightarrow ((\neg (\neg φ \to φ) \lor (ψ \to χ)) \land ((\neg φ \to φ) \lor (θ \to τ)))$
19		ifpim123g	$⊢ (if- (φ, ψ, θ) \to if- (φ, χ, τ)) \leftrightarrow ((((φ \to \neg φ) \lor (ψ \to χ)) \land ((φ \to φ) \lor (θ \to χ))) \land (((φ \to φ) \lor (ψ \to τ)) \land ((\neg φ \to φ) \lor (θ \to τ))))$
20	12 18 19	3imtr4i	$⊢ if- (φ, (ψ \to χ), (θ \to τ)) \to (if- (φ, ψ, θ) \to if- (φ, χ, τ))$

Metamath Proof Explorer

Theorem ifpimim

Proof