plvcofphax

Description: Given, a,b,d, and "definitions" for c, e, f, g: g is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020)

	Ref	Expression
Hypotheses	plvcofphax.1	$⊢ χ \leftrightarrow ((((φ \land ψ) \leftrightarrow φ) \to (φ \land \neg (φ \land \neg φ))) \land (φ \land \neg (φ \land \neg φ)))$
	plvcofphax.2	$⊢ τ \leftrightarrow ((χ \to θ) \land (φ \leftrightarrow χ) \land ((φ \to ψ) \to (ψ \leftrightarrow θ)))$
	plvcofphax.3	$⊢ η \leftrightarrow (χ \land τ)$
	plvcofphax.4	$⊢ φ$
	plvcofphax.5	$⊢ ψ$
	plvcofphax.6	$⊢ θ$
	plvcofphax.7	$⊢ ζ \leftrightarrow \neg (ψ \land \neg τ)$
Assertion	plvcofphax	$⊢ ζ$

Step	Hyp	Ref	Expression
1		plvcofphax.1	$⊢ χ \leftrightarrow ((((φ \land ψ) \leftrightarrow φ) \to (φ \land \neg (φ \land \neg φ))) \land (φ \land \neg (φ \land \neg φ)))$
2		plvcofphax.2	$⊢ τ \leftrightarrow ((χ \to θ) \land (φ \leftrightarrow χ) \land ((φ \to ψ) \to (ψ \leftrightarrow θ)))$
3		plvcofphax.3	$⊢ η \leftrightarrow (χ \land τ)$
4		plvcofphax.4	$⊢ φ$
5		plvcofphax.5	$⊢ ψ$
6		plvcofphax.6	$⊢ θ$
7		plvcofphax.7	$⊢ ζ \leftrightarrow \neg (ψ \land \neg τ)$
8	1 4 5	plcofph	$⊢ χ$
9	2 4 5 8 6	pldofph	$⊢ τ$
10	5 9	pm3.2i	$⊢ (ψ \land τ)$
11		pm3.4	$⊢ (ψ \land τ) \to (ψ \to τ)$
12	10 11	ax-mp	$⊢ ψ \to τ$
13		iman	$⊢ (ψ \to τ) \leftrightarrow \neg (ψ \land \neg τ)$
14	13	biimpi	$⊢ (ψ \to τ) \to \neg (ψ \land \neg τ)$
15	12 14	ax-mp	$⊢ \neg (ψ \land \neg τ)$
16	7	bicomi	$⊢ \neg (ψ \land \neg τ) \leftrightarrow ζ$
17	16	biimpi	$⊢ \neg (ψ \land \neg τ) \to ζ$
18	15 17	ax-mp	$⊢ ζ$

Metamath Proof Explorer