Metamath Proof Explorer


Theorem 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 χ¬φ¬ψ
plvofpos.2 θ¬φψ
plvofpos.3 τφ¬ψ
plvofpos.4 ηφψ
plvofpos.5 ζ¬μχμθ¬μχμτ¬μχχη¬μθμτ¬μθμη¬μτμη
plvofpos.6 σμχμθμτμη
plvofpos.7 ρζσ
plvofpos.8 ζ
plvofpos.9 σ
Assertion plvofpos ρ

Proof

Step Hyp Ref Expression
1 plvofpos.1 χ¬φ¬ψ
2 plvofpos.2 θ¬φψ
3 plvofpos.3 τφ¬ψ
4 plvofpos.4 ηφψ
5 plvofpos.5 ζ¬μχμθ¬μχμτ¬μχχη¬μθμτ¬μθμη¬μτμη
6 plvofpos.6 σμχμθμτμη
7 plvofpos.7 ρζσ
8 plvofpos.8 ζ
9 plvofpos.9 σ
10 8 9 pm3.2i ζσ
11 7 bicomi ζσρ
12 11 biimpi ζσρ
13 10 12 ax-mp ρ