Theorem nic-ax

Description: Nicod's axiom derived from the standard ones. SeeIntroduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith , the usual axioms can be derived from this and vice versa. Unlike meredith , Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g., { nic-ax , nic-mp } is equivalent to { luk-1 , luk-2 , luk-3 , ax-mp } . In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to an axiom ($a statement). (Contributed by Jeff Hoffman, 19-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	nic-ax	⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ⊼ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		nannan	⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ↔ ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) )
2	1	biimpi	⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) → ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) )
3		simpl	⊢ ( ( 𝜒 ∧ 𝜓 ) → 𝜒 )
4	3	imim2i	⊢ ( ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) → ( 𝜑 → 𝜒 ) )
5		imnan	⊢ ( ( 𝜃 → ¬ 𝜒 ) ↔ ¬ ( 𝜃 ∧ 𝜒 ) )
6		df-nan	⊢ ( ( 𝜃 ⊼ 𝜒 ) ↔ ¬ ( 𝜃 ∧ 𝜒 ) )
7	5 6	bitr4i	⊢ ( ( 𝜃 → ¬ 𝜒 ) ↔ ( 𝜃 ⊼ 𝜒 ) )
8		con3	⊢ ( ( 𝜑 → 𝜒 ) → ( ¬ 𝜒 → ¬ 𝜑 ) )
9	8	imim2d	⊢ ( ( 𝜑 → 𝜒 ) → ( ( 𝜃 → ¬ 𝜒 ) → ( 𝜃 → ¬ 𝜑 ) ) )
10		imnan	⊢ ( ( 𝜑 → ¬ 𝜃 ) ↔ ¬ ( 𝜑 ∧ 𝜃 ) )
11		con2b	⊢ ( ( 𝜃 → ¬ 𝜑 ) ↔ ( 𝜑 → ¬ 𝜃 ) )
12		df-nan	⊢ ( ( 𝜑 ⊼ 𝜃 ) ↔ ¬ ( 𝜑 ∧ 𝜃 ) )
13	10 11 12	3bitr4ri	⊢ ( ( 𝜑 ⊼ 𝜃 ) ↔ ( 𝜃 → ¬ 𝜑 ) )
14	9 13	syl6ibr	⊢ ( ( 𝜑 → 𝜒 ) → ( ( 𝜃 → ¬ 𝜒 ) → ( 𝜑 ⊼ 𝜃 ) ) )
15	7 14	syl5bir	⊢ ( ( 𝜑 → 𝜒 ) → ( ( 𝜃 ⊼ 𝜒 ) → ( 𝜑 ⊼ 𝜃 ) ) )
16		nanim	⊢ ( ( ( 𝜃 ⊼ 𝜒 ) → ( 𝜑 ⊼ 𝜃 ) ) ↔ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) )
17	15 16	sylib	⊢ ( ( 𝜑 → 𝜒 ) → ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) )
18	2 4 17	3syl	⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) → ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) )
19		pm4.24	⊢ ( 𝜏 ↔ ( 𝜏 ∧ 𝜏 ) )
20	19	biimpi	⊢ ( 𝜏 → ( 𝜏 ∧ 𝜏 ) )
21		nannan	⊢ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ↔ ( 𝜏 → ( 𝜏 ∧ 𝜏 ) ) )
22	20 21	mpbir	⊢ ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) )
23	18 22	jctil	⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) → ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ∧ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) )
24		nannan	⊢ ( ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ⊼ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) ) ↔ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) → ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ∧ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) ) )
25	23 24	mpbir	⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ⊼ ( ( 𝜏 ⊼ ( 𝜏 ⊼ 𝜏 ) ) ⊼ ( ( 𝜃 ⊼ 𝜒 ) ⊼ ( ( 𝜑 ⊼ 𝜃 ) ⊼ ( 𝜑 ⊼ 𝜃 ) ) ) ) )