plcofph

Description: Given, a,b and a "definition" for c, c is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020)

	Ref	Expression
Hypotheses	plcofph.1	$⊢ χ \leftrightarrow ((((φ \land ψ) \leftrightarrow φ) \to (φ \land \neg (φ \land \neg φ))) \land (φ \land \neg (φ \land \neg φ)))$
	plcofph.2	$⊢ φ$
	plcofph.3	$⊢ ψ$
Assertion	plcofph	$⊢ χ$

Step	Hyp	Ref	Expression
1		plcofph.1	$⊢ χ \leftrightarrow ((((φ \land ψ) \leftrightarrow φ) \to (φ \land \neg (φ \land \neg φ))) \land (φ \land \neg (φ \land \neg φ)))$
2		plcofph.2	$⊢ φ$
3		plcofph.3	$⊢ ψ$
4		pm3.24	$⊢ \neg (φ \land \neg φ)$
5	2 4	pm3.2i	$⊢ (φ \land \neg (φ \land \neg φ))$
6	5	a1i	$⊢ ((φ \land ψ) \leftrightarrow φ) \to (φ \land \neg (φ \land \neg φ))$
7	6 5	pm3.2i	$⊢ ((((φ \land ψ) \leftrightarrow φ) \to (φ \land \neg (φ \land \neg φ))) \land (φ \land \neg (φ \land \neg φ)))$
8	1	bicomi	$⊢ ((((φ \land ψ) \leftrightarrow φ) \to (φ \land \neg (φ \land \neg φ))) \land (φ \land \neg (φ \land \neg φ))) \leftrightarrow χ$
9	8	biimpi	$⊢ ((((φ \land ψ) \leftrightarrow φ) \to (φ \land \neg (φ \land \neg φ))) \land (φ \land \neg (φ \land \neg φ))) \to χ$
10	7 9	ax-mp	$⊢ χ$

Metamath Proof Explorer