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 40870 is con3ALTVD 41256 without
virtual deductions and was automatically derived from con3ALTVD 41256.
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 40914 | . . . . . 6 ⊢ ( (𝜑 → 𝜓) ▶ (𝜑 → 𝜓) ) | |
2 | idn2 40953 | . . . . . . 7 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ ¬ ¬ 𝜑 ) | |
3 | notnotr 132 | . . . . . . 7 ⊢ (¬ ¬ 𝜑 → 𝜑) | |
4 | 2, 3 | e2 40971 | . . . . . 6 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ 𝜑 ) |
5 | id 22 | . . . . . 6 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓)) | |
6 | 1, 4, 5 | e12 41064 | . . . . 5 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ 𝜓 ) |
7 | notnot 144 | . . . . 5 ⊢ (𝜓 → ¬ ¬ 𝜓) | |
8 | 6, 7 | e2 40971 | . . . 4 ⊢ ( (𝜑 → 𝜓) , ¬ ¬ 𝜑 ▶ ¬ ¬ 𝜓 ) |
9 | 8 | in2 40945 | . . 3 ⊢ ( (𝜑 → 𝜓) ▶ (¬ ¬ 𝜑 → ¬ ¬ 𝜓) ) |
10 | con4 113 | . . 3 ⊢ ((¬ ¬ 𝜑 → ¬ ¬ 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | |
11 | 9, 10 | e1a 40967 | . 2 ⊢ ( (𝜑 → 𝜓) ▶ (¬ 𝜓 → ¬ 𝜑) ) |
12 | 11 | in1 40911 | 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 209 df-an 399 df-vd1 40910 df-vd2 40918 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |