plvofpos

Description: rh is derivable because ONLY one of ch, th, ta, et is implied by mu. (Contributed by Jarvin Udandy, 11-Sep-2020)

	Ref	Expression
Hypotheses	plvofpos.1	$⊢ χ \leftrightarrow (\neg φ \land \neg ψ)$
	plvofpos.2	$⊢ θ \leftrightarrow (\neg φ \land ψ)$
	plvofpos.3	$⊢ τ \leftrightarrow (φ \land \neg ψ)$
	plvofpos.4	$⊢ η \leftrightarrow (φ \land ψ)$
	plvofpos.5	$⊢ ζ \leftrightarrow (((((\neg ((μ \to χ) \land (μ \to θ)) \land \neg ((μ \to χ) \land (μ \to τ))) \land \neg ((μ \to χ) \land (χ \to η))) \land \neg ((μ \to θ) \land (μ \to τ))) \land \neg ((μ \to θ) \land (μ \to η))) \land \neg ((μ \to τ) \land (μ \to η)))$
	plvofpos.6	$⊢ σ \leftrightarrow (((μ \to χ) \lor (μ \to θ)) \lor ((μ \to τ) \lor (μ \to η)))$
	plvofpos.7	$⊢ ρ \leftrightarrow (ζ \land σ)$
	plvofpos.8	$⊢ ζ$
	plvofpos.9	$⊢ σ$
Assertion	plvofpos	$⊢ ρ$

Step	Hyp	Ref	Expression
1		plvofpos.1	$⊢ χ \leftrightarrow (\neg φ \land \neg ψ)$
2		plvofpos.2	$⊢ θ \leftrightarrow (\neg φ \land ψ)$
3		plvofpos.3	$⊢ τ \leftrightarrow (φ \land \neg ψ)$
4		plvofpos.4	$⊢ η \leftrightarrow (φ \land ψ)$
5		plvofpos.5	$⊢ ζ \leftrightarrow (((((\neg ((μ \to χ) \land (μ \to θ)) \land \neg ((μ \to χ) \land (μ \to τ))) \land \neg ((μ \to χ) \land (χ \to η))) \land \neg ((μ \to θ) \land (μ \to τ))) \land \neg ((μ \to θ) \land (μ \to η))) \land \neg ((μ \to τ) \land (μ \to η)))$
6		plvofpos.6	$⊢ σ \leftrightarrow (((μ \to χ) \lor (μ \to θ)) \lor ((μ \to τ) \lor (μ \to η)))$
7		plvofpos.7	$⊢ ρ \leftrightarrow (ζ \land σ)$
8		plvofpos.8	$⊢ ζ$
9		plvofpos.9	$⊢ σ$
10	8 9	pm3.2i	$⊢ (ζ \land σ)$
11	7	bicomi	$⊢ (ζ \land σ) \leftrightarrow ρ$
12	11	biimpi	$⊢ (ζ \land σ) \to ρ$
13	10 12	ax-mp	$⊢ ρ$

Metamath Proof Explorer