Metamath Proof Explorer

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 
|- ( ( ph -/\ ( ch -/\ ps ) ) -/\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )

Proof

Step Hyp Ref Expression
1 nannan 
 |-  ( ( ph -/\ ( ch -/\ ps ) ) <-> ( ph -> ( ch /\ ps ) ) )
2 1 biimpi 
 |-  ( ( ph -/\ ( ch -/\ ps ) ) -> ( ph -> ( ch /\ ps ) ) )
3 simpl 
 |-  ( ( ch /\ ps ) -> ch )
4 3 imim2i 
 |-  ( ( ph -> ( ch /\ ps ) ) -> ( ph -> ch ) )
5 imnan 
 |-  ( ( th -> -. ch ) <-> -. ( th /\ ch ) )
6 df-nan 
 |-  ( ( th -/\ ch ) <-> -. ( th /\ ch ) )
7 5 6 bitr4i 
 |-  ( ( th -> -. ch ) <-> ( th -/\ ch ) )
8 con3 
 |-  ( ( ph -> ch ) -> ( -. ch -> -. ph ) )
9 8 imim2d 
 |-  ( ( ph -> ch ) -> ( ( th -> -. ch ) -> ( th -> -. ph ) ) )
10 imnan 
 |-  ( ( ph -> -. th ) <-> -. ( ph /\ th ) )
11 con2b 
 |-  ( ( th -> -. ph ) <-> ( ph -> -. th ) )
12 df-nan 
 |-  ( ( ph -/\ th ) <-> -. ( ph /\ th ) )
13 10 11 12 3bitr4ri 
 |-  ( ( ph -/\ th ) <-> ( th -> -. ph ) )
14 9 13 imbitrrdi 
 |-  ( ( ph -> ch ) -> ( ( th -> -. ch ) -> ( ph -/\ th ) ) )
15 7 14 biimtrrid 
 |-  ( ( ph -> ch ) -> ( ( th -/\ ch ) -> ( ph -/\ th ) ) )
16 nanim 
 |-  ( ( ( th -/\ ch ) -> ( ph -/\ th ) ) <-> ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) )
17 15 16 sylib 
 |-  ( ( ph -> ch ) -> ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) )
18 2 4 17 3syl 
 |-  ( ( ph -/\ ( ch -/\ ps ) ) -> ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) )
19 pm4.24 
 |-  ( ta <-> ( ta /\ ta ) )
20 19 biimpi 
 |-  ( ta -> ( ta /\ ta ) )
21 nannan 
 |-  ( ( ta -/\ ( ta -/\ ta ) ) <-> ( ta -> ( ta /\ ta ) ) )
22 20 21 mpbir 
 |-  ( ta -/\ ( ta -/\ ta ) )
23 18 22 jctil 
 |-  ( ( ph -/\ ( ch -/\ ps ) ) -> ( ( ta -/\ ( ta -/\ ta ) ) /\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )
24 nannan 
 |-  ( ( ( ph -/\ ( ch -/\ ps ) ) -/\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) ) <-> ( ( ph -/\ ( ch -/\ ps ) ) -> ( ( ta -/\ ( ta -/\ ta ) ) /\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) ) )
25 23 24 mpbir 
 |-  ( ( ph -/\ ( ch -/\ ps ) ) -/\ ( ( ta -/\ ( ta -/\ ta ) ) -/\ ( ( th -/\ ch ) -/\ ( ( ph -/\ th ) -/\ ( ph -/\ th ) ) ) ) )