![]() |
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 43291 is con3ALTVD 43677 without
virtual deductions and was automatically derived from con3ALTVD 43677.
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 43335 | . . . . . 6 ⊢ ( (𝜑 → 𝜓) ▶ (𝜑 → 𝜓) ) | |
2 | idn2 43374 | . . . . . . 7 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ ¬ ¬ 𝜑 ) | |
3 | notnotr 130 | . . . . . . 7 ⊢ (¬ ¬ 𝜑 → 𝜑) | |
4 | 2, 3 | e2 43392 | . . . . . 6 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ 𝜑 ) |
5 | id 22 | . . . . . 6 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓)) | |
6 | 1, 4, 5 | e12 43485 | . . . . 5 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ 𝜓 ) |
7 | notnot 142 | . . . . 5 ⊢ (𝜓 → ¬ ¬ 𝜓) | |
8 | 6, 7 | e2 43392 | . . . 4 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ ¬ ¬ 𝜓 ) |
9 | 8 | in2 43366 | . . 3 ⊢ ( (𝜑 → 𝜓) ▶ (¬ ¬ 𝜑 → ¬ ¬ 𝜓) ) |
10 | con4 113 | . . 3 ⊢ ((¬ ¬ 𝜑 → ¬ ¬ 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | |
11 | 9, 10 | e1a 43388 | . 2 ⊢ ( (𝜑 → 𝜓) ▶ (¬ 𝜓 → ¬ 𝜑) ) |
12 | 11 | in1 43332 | 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 398 df-vd1 43331 df-vd2 43339 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |