Mathbox for Jarvin Udandy < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  plvofpos Structured version   Visualization version   GIF version

Theorem plvofpos 39764
 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
StepHypRef Expression
1 plvofpos.8 . . 3 𝜁
2 plvofpos.9 . . 3 𝜎
31, 2pm3.2i 470 . 2 (𝜁𝜎)
4 plvofpos.7 . . . 4 (𝜌 ↔ (𝜁𝜎))
54bicomi 213 . . 3 ((𝜁𝜎) ↔ 𝜌)
65biimpi 205 . 2 ((𝜁𝜎) → 𝜌)
73, 6ax-mp 5 1 𝜌
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383 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 196  df-an 385 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator