![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > con3ALTVD | Structured version Visualization version GIF version |
Description: The following User's Proof is a Natural Deduction Sequent Calculus
transcription of the Fitch-style Natural Deduction proof of Theorem 7 of
Section 14 of [Margaris] p. 60 (which is con3 153). The same proof may
also be interpreted to be a Virtual Deduction Hilbert-style axiomatic
proof. It was completed automatically by the tools program
completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm
Megill's Metamath Proof Assistant. con3ALT2 43281 is con3ALTVD 43667 without
virtual deductions and was automatically derived from con3ALTVD 43667.
Step i of the User's Proof corresponds to step i of the Fitch-style proof.
|
Ref | Expression |
---|---|
con3ALTVD | ⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | idn1 43325 | . . . . . 6 ⊢ ( (𝜑 → 𝜓) ▶ (𝜑 → 𝜓) ) | |
2 | idn2 43364 | . . . . . . 7 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ ¬ ¬ 𝜑 ) | |
3 | notnotr 130 | . . . . . . 7 ⊢ (¬ ¬ 𝜑 → 𝜑) | |
4 | 2, 3 | e2 43382 | . . . . . 6 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ 𝜑 ) |
5 | id 22 | . . . . . 6 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓)) | |
6 | 1, 4, 5 | e12 43475 | . . . . 5 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ 𝜓 ) |
7 | notnot 142 | . . . . 5 ⊢ (𝜓 → ¬ ¬ 𝜓) | |
8 | 6, 7 | e2 43382 | . . . 4 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ ¬ ¬ 𝜓 ) |
9 | 8 | in2 43356 | . . 3 ⊢ ( (𝜑 → 𝜓) ▶ (¬ ¬ 𝜑 → ¬ ¬ 𝜓) ) |
10 | con4 113 | . . 3 ⊢ ((¬ ¬ 𝜑 → ¬ ¬ 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | |
11 | 9, 10 | e1a 43378 | . 2 ⊢ ( (𝜑 → 𝜓) ▶ (¬ 𝜓 → ¬ 𝜑) ) |
12 | 11 | in1 43322 | 1 ⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 |
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 206 df-an 397 df-vd1 43321 df-vd2 43329 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |