Theorem plvofpos 46965

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

Hypotheses

Ref	Expression
plvofpos.1	⊢ (𝜒 ↔ (¬ 𝜑 ∧ ¬ 𝜓))
plvofpos.2	⊢ (𝜃 ↔ (¬ 𝜑 ∧ 𝜓))
plvofpos.3	⊢ (𝜏 ↔ (𝜑 ∧ ¬ 𝜓))
plvofpos.4	⊢ (𝜂 ↔ (𝜑 ∧ 𝜓))
plvofpos.5	⊢ (𝜁 ↔ (((((¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜃)) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜒) ∧ (𝜒 → 𝜂))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜏))) ∧ ¬ ((𝜇 → 𝜃) ∧ (𝜇 → 𝜂))) ∧ ¬ ((𝜇 → 𝜏) ∧ (𝜇 → 𝜂))))
plvofpos.6	⊢ (𝜎 ↔ (((𝜇 → 𝜒) ∨ (𝜇 → 𝜃)) ∨ ((𝜇 → 𝜏) ∨ (𝜇 → 𝜂))))
plvofpos.7	⊢ (𝜌 ↔ (𝜁 ∧ 𝜎))
plvofpos.8	⊢ 𝜁
plvofpos.9	⊢ 𝜎

Assertion

Ref	Expression
plvofpos	⊢ 𝜌

Proof of Theorem plvofpos

Step	Hyp	Ref	Expression
1		plvofpos.8	. . 3 ⊢ 𝜁
2		plvofpos.9	. . 3 ⊢ 𝜎
3	1, 2	pm3.2i 470	. 2 ⊢ (𝜁 ∧ 𝜎)
4		plvofpos.7	. . . 4 ⊢ (𝜌 ↔ (𝜁 ∧ 𝜎))
5	4	bicomi 224	. . 3 ⊢ ((𝜁 ∧ 𝜎) ↔ 𝜌)
6	5	biimpi 216	. 2 ⊢ ((𝜁 ∧ 𝜎) → 𝜌)
7	3, 6	ax-mp 5	1 ⊢ 𝜌

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by: (None)