![]() |
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 42904 is con3ALTVD 43290 without
virtual deductions and was automatically derived from con3ALTVD 43290.
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 42948 | . . . . . 6 ⊢ ( (𝜑 → 𝜓) ▶ (𝜑 → 𝜓) ) | |
2 | idn2 42987 | . . . . . . 7 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ ¬ ¬ 𝜑 ) | |
3 | notnotr 130 | . . . . . . 7 ⊢ (¬ ¬ 𝜑 → 𝜑) | |
4 | 2, 3 | e2 43005 | . . . . . 6 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ 𝜑 ) |
5 | id 22 | . . . . . 6 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓)) | |
6 | 1, 4, 5 | e12 43098 | . . . . 5 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ 𝜓 ) |
7 | notnot 142 | . . . . 5 ⊢ (𝜓 → ¬ ¬ 𝜓) | |
8 | 6, 7 | e2 43005 | . . . 4 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ ¬ ¬ 𝜓 ) |
9 | 8 | in2 42979 | . . 3 ⊢ ( (𝜑 → 𝜓) ▶ (¬ ¬ 𝜑 → ¬ ¬ 𝜓) ) |
10 | con4 113 | . . 3 ⊢ ((¬ ¬ 𝜑 → ¬ ¬ 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | |
11 | 9, 10 | e1a 43001 | . 2 ⊢ ( (𝜑 → 𝜓) ▶ (¬ 𝜓 → ¬ 𝜑) ) |
12 | 11 | in1 42945 | 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 42944 df-vd2 42952 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |