![]() |
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 156). 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 41236 is con3ALTVD 41622 without
virtual deductions and was automatically derived from con3ALTVD 41622.
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 41280 | . . . . . 6 ⊢ ( (𝜑 → 𝜓) ▶ (𝜑 → 𝜓) ) | |
2 | idn2 41319 | . . . . . . 7 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ ¬ ¬ 𝜑 ) | |
3 | notnotr 132 | . . . . . . 7 ⊢ (¬ ¬ 𝜑 → 𝜑) | |
4 | 2, 3 | e2 41337 | . . . . . 6 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ 𝜑 ) |
5 | id 22 | . . . . . 6 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓)) | |
6 | 1, 4, 5 | e12 41430 | . . . . 5 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ 𝜓 ) |
7 | notnot 144 | . . . . 5 ⊢ (𝜓 → ¬ ¬ 𝜓) | |
8 | 6, 7 | e2 41337 | . . . 4 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ ¬ ¬ 𝜓 ) |
9 | 8 | in2 41311 | . . 3 ⊢ ( (𝜑 → 𝜓) ▶ (¬ ¬ 𝜑 → ¬ ¬ 𝜓) ) |
10 | con4 113 | . . 3 ⊢ ((¬ ¬ 𝜑 → ¬ ¬ 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | |
11 | 9, 10 | e1a 41333 | . 2 ⊢ ( (𝜑 → 𝜓) ▶ (¬ 𝜓 → ¬ 𝜑) ) |
12 | 11 | in1 41277 | 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 210 df-an 400 df-vd1 41276 df-vd2 41284 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |