Theorem notnotrALTVD 41247

Description: The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Theorem 5 of Section 14 of [Margaris] p. 59 (which is notnotr 132). The same proof may also be interpreted as 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. notnotrALT 40861 is notnotrALTVD 41247 without virtual deductions and was automatically derived from notnotrALTVD 41247. Step i of the User's Proof corresponds to step i of the Fitch-style proof.

1::	⊢ (   ¬ ¬ 𝜑   ▶   ¬ ¬ 𝜑   )
2::	⊢ (¬ ¬ 𝜑 → (¬ 𝜑 → ¬ ¬ ¬ 𝜑))
3:1:	⊢ (   ¬ ¬ 𝜑   ▶   (¬ 𝜑 → ¬ ¬ ¬ 𝜑)   )
4::	⊢ ((¬ 𝜑 → ¬ ¬ ¬ 𝜑) → (¬ ¬ 𝜑 → 𝜑))
5:3:	⊢ (   ¬ ¬ 𝜑   ▶   (¬ ¬ 𝜑 → 𝜑)   )
6:5,1:	⊢ (   ¬ ¬ 𝜑   ▶   𝜑   )
qed:6:	⊢ (¬ ¬ 𝜑 → 𝜑)

(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
notnotrALTVD	⊢ (¬ ¬ 𝜑 → 𝜑)

Proof of Theorem notnotrALTVD

Step	Hyp	Ref	Expression
1		idn1 40906	. . . . 5 ⊢ (    ¬ ¬ 𝜑   ▶    ¬ ¬ 𝜑   )
2		pm2.21 123	. . . . 5 ⊢ (¬ ¬ 𝜑 → (¬ 𝜑 → ¬ ¬ ¬ 𝜑))
3	1, 2	e1a 40959	. . . 4 ⊢ (    ¬ ¬ 𝜑   ▶   (¬ 𝜑 → ¬ ¬ ¬ 𝜑)   )
4		con4 113	. . . 4 ⊢ ((¬ 𝜑 → ¬ ¬ ¬ 𝜑) → (¬ ¬ 𝜑 → 𝜑))
5	3, 4	e1a 40959	. . 3 ⊢ (    ¬ ¬ 𝜑   ▶   (¬ ¬ 𝜑 → 𝜑)   )
6		id 22	. . 3 ⊢ ((¬ ¬ 𝜑 → 𝜑) → (¬ ¬ 𝜑 → 𝜑))
7	5, 1, 6	e11 41020	. 2 ⊢ (    ¬ ¬ 𝜑   ▶   𝜑   )
8	7	in1 40903	1 ⊢ (¬ ¬ 𝜑 → 𝜑)

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-vd1 40902

This theorem is referenced by: (None)