|   | Mathbox for Alan Sare | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > un0.1 | Structured version Visualization version GIF version | ||
| Description: ⊤ is the constant true, a tautology (see df-tru 1543). Kleene's "empty conjunction" is logically equivalent to ⊤. In a virtual deduction we shall interpret ⊤ to be the empty wff or the empty collection of virtual hypotheses. ⊤ in a virtual deduction translated into conventional notation we shall interpret to be Kleene's empty conjunction. If 𝜃 is true given the empty collection of virtual hypotheses and another collection of virtual hypotheses, then it is true given only the other collection of virtual hypotheses. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.) | 
| Ref | Expression | 
|---|---|
| un0.1.1 | ⊢ ( ⊤ ▶ 𝜑 ) | 
| un0.1.2 | ⊢ ( 𝜓 ▶ 𝜒 ) | 
| un0.1.3 | ⊢ ( ( ⊤ , 𝜓 ) ▶ 𝜃 ) | 
| Ref | Expression | 
|---|---|
| un0.1 | ⊢ ( 𝜓 ▶ 𝜃 ) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | un0.1.1 | . . . 4 ⊢ ( ⊤ ▶ 𝜑 ) | |
| 2 | 1 | in1 44591 | . . 3 ⊢ (⊤ → 𝜑) | 
| 3 | un0.1.2 | . . . 4 ⊢ ( 𝜓 ▶ 𝜒 ) | |
| 4 | 3 | in1 44591 | . . 3 ⊢ (𝜓 → 𝜒) | 
| 5 | un0.1.3 | . . . 4 ⊢ ( ( ⊤ , 𝜓 ) ▶ 𝜃 ) | |
| 6 | 5 | dfvd2ani 44603 | . . 3 ⊢ ((⊤ ∧ 𝜓) → 𝜃) | 
| 7 | 2, 4, 6 | uun0.1 44798 | . 2 ⊢ (𝜓 → 𝜃) | 
| 8 | 7 | dfvd1ir 44593 | 1 ⊢ ( 𝜓 ▶ 𝜃 ) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ⊤wtru 1541 ( wvd1 44589 ( wvhc2 44600 | 
| 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 df-tru 1543 df-vd1 44590 df-vhc2 44601 | 
| This theorem is referenced by: sspwimpVD 44939 | 
| Copyright terms: Public domain | W3C validator |