3impexpVD

Description: Virtual deduction proof of 3impexp . The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

		Ref	Expression
	Assertion	3impexpVD	$⊢ ((φ \land ψ \land χ) \to θ) \leftrightarrow (φ \to (ψ \to (χ \to θ)))$

Proof

Step	Hyp	Ref	Expression
1		idn1	$⊢ (((φ \land ψ \land χ) \to θ) \to ((φ \land ψ \land χ) \to θ))$
2		df-3an	$⊢ (φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land χ)$
3		imbi1	$⊢ ((φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land χ)) \to (((φ \land ψ \land χ) \to θ) \leftrightarrow (((φ \land ψ) \land χ) \to θ))$
4	3	biimpcd	$⊢ ((φ \land ψ \land χ) \to θ) \to (((φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land χ)) \to (((φ \land ψ) \land χ) \to θ))$
5	1 2 4	e10	$⊢ (((φ \land ψ \land χ) \to θ) \to (((φ \land ψ) \land χ) \to θ))$
6		pm3.3	$⊢ (((φ \land ψ) \land χ) \to θ) \to ((φ \land ψ) \to (χ \to θ))$
7	5 6	e1a	$⊢ (((φ \land ψ \land χ) \to θ) \to ((φ \land ψ) \to (χ \to θ)))$
8		pm3.3	$⊢ ((φ \land ψ) \to (χ \to θ)) \to (φ \to (ψ \to (χ \to θ)))$
9	7 8	e1a	$⊢ (((φ \land ψ \land χ) \to θ) \to (φ \to (ψ \to (χ \to θ))))$
10	9	in1	$⊢ ((φ \land ψ \land χ) \to θ) \to (φ \to (ψ \to (χ \to θ)))$
11		idn1	$⊢ ((φ \to (ψ \to (χ \to θ))) \to (φ \to (ψ \to (χ \to θ))))$
12		pm3.31	$⊢ (φ \to (ψ \to (χ \to θ))) \to ((φ \land ψ) \to (χ \to θ))$
13	11 12	e1a	$⊢ ((φ \to (ψ \to (χ \to θ))) \to ((φ \land ψ) \to (χ \to θ)))$
14		pm3.31	$⊢ ((φ \land ψ) \to (χ \to θ)) \to (((φ \land ψ) \land χ) \to θ)$
15	13 14	e1a	$⊢ ((φ \to (ψ \to (χ \to θ))) \to (((φ \land ψ) \land χ) \to θ))$
16	3	biimprd	$⊢ ((φ \land ψ \land χ) \leftrightarrow ((φ \land ψ) \land χ)) \to ((((φ \land ψ) \land χ) \to θ) \to ((φ \land ψ \land χ) \to θ))$
17	2 15 16	e01	$⊢ ((φ \to (ψ \to (χ \to θ))) \to ((φ \land ψ \land χ) \to θ))$
18	17	in1	$⊢ (φ \to (ψ \to (χ \to θ))) \to ((φ \land ψ \land χ) \to θ)$
19		impbi	$⊢ (((φ \land ψ \land χ) \to θ) \to (φ \to (ψ \to (χ \to θ)))) \to (((φ \to (ψ \to (χ \to θ))) \to ((φ \land ψ \land χ) \to θ)) \to (((φ \land ψ \land χ) \to θ) \leftrightarrow (φ \to (ψ \to (χ \to θ)))))$
20	10 18 19	e00	$⊢ ((φ \land ψ \land χ) \to θ) \leftrightarrow (φ \to (ψ \to (χ \to θ)))$

1::	\|- (. ( ( ph /\ ps /\ ch ) -> th ) ->. ( ( ph /\ ps /\ ch ) -> th ) ).
2::	\|- ( ( ph /\ ps /\ ch ) <-> ( ( ph /\ ps ) /\ ch ) )
3:1,2,?: e10	\|- (. ( ( ph /\ ps /\ ch ) -> th ) ->. ( ( ( ph /\ ps ) /\ ch ) -> th ) ).
4:3,?: e1a	\|- (. ( ( ph /\ ps /\ ch ) -> th ) ->. ( ( ph /\ ps ) -> ( ch -> th ) ) ).
5:4,?: e1a	\|- (. ( ( ph /\ ps /\ ch ) -> th ) ->. ( ph -> ( ps -> ( ch -> th ) ) ) ).
6:5:	\|- ( ( ( ph /\ ps /\ ch ) -> th ) -> ( ph -> ( ps -> ( ch -> th ) ) ) )
7::	\|- (. ( ph -> ( ps -> ( ch -> th ) ) ) ->. ( ph -> ( ps -> ( ch -> th ) ) ) ).
8:7,?: e1a	\|- (. ( ph -> ( ps -> ( ch -> th ) ) ) ->. ( ( ph /\ ps ) -> ( ch -> th ) ) ).
9:8,?: e1a	\|- (. ( ph -> ( ps -> ( ch -> th ) ) ) ->. ( ( ( ph /\ ps ) /\ ch ) -> th ) ).
10:2,9,?: e01	\|- (. ( ph -> ( ps -> ( ch -> th ) ) ) ->. ( ( ph /\ ps /\ ch ) -> th ) ).
11:10:	\|- ( ( ph -> ( ps -> ( ch -> th ) ) ) -> ( ( ph /\ ps /\ ch ) -> th ) )
qed:6,11,?: e00	\|- ( ( ( ph /\ ps /\ ch ) -> th ) <-> ( ph -> ( ps -> ( ch -> th ) ) ) )

Metamath Proof Explorer

Theorem 3impexpVD

Proof