Metamath Proof Explorer
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 |
⊢ 𝜌 |