New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax-meredith GIF version

Axiom ax-meredith 1406
 Description: Theorem meredith 1404 restated as an axiom. This will allow us to ensure that the rederivation of ax1 1431, ax2 1432, and ax3 1433 below depend only on Meredith's sole axiom and not accidentally on a previous theorem above. Outside of this section, we will not make use of this axiom. (Contributed by NM, 14-Dec-2002.) (New usage is discouraged.)
Assertion
Ref Expression
ax-meredith (((((φψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τφ) → (θφ)))

Detailed syntax breakdown of Axiom ax-meredith
StepHypRef Expression
1 wph . . . . . 6 wff φ
2 wps . . . . . 6 wff ψ
31, 2wi 4 . . . . 5 wff (φψ)
4 wch . . . . . . 7 wff χ
54wn 3 . . . . . 6 wff ¬ χ
6 wth . . . . . . 7 wff θ
76wn 3 . . . . . 6 wff ¬ θ
85, 7wi 4 . . . . 5 wff χ → ¬ θ)
93, 8wi 4 . . . 4 wff ((φψ) → (¬ χ → ¬ θ))
109, 4wi 4 . . 3 wff (((φψ) → (¬ χ → ¬ θ)) → χ)
11 wta . . 3 wff τ
1210, 11wi 4 . 2 wff ((((φψ) → (¬ χ → ¬ θ)) → χ) → τ)
1311, 1wi 4 . . 3 wff (τφ)
146, 1wi 4 . . 3 wff (θφ)
1513, 14wi 4 . 2 wff ((τφ) → (θφ))
1612, 15wi 4 1 wff (((((φψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τφ) → (θφ)))
 Colors of variables: wff setvar class This axiom is referenced by:  merlem1  1407  merlem2  1408  merlem3  1409  merlem4  1410  merlem5  1411  merlem7  1413  merlem8  1414  merlem9  1415  merlem10  1416  merlem11  1417  merlem13  1419  luk-1  1420  luk-2  1421
 Copyright terms: Public domain W3C validator