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

Step	Hyp	Ref	Expression
1		wph	. . . . . 6 wff φ
2		wps	. . . . . 6 wff ψ
3	1, 2	wi 4	. . . . 5 wff (φ → ψ)
4		wch	. . . . . . 7 wff χ
5	4	wn 3	. . . . . 6 wff ¬ χ
6		wth	. . . . . . 7 wff θ
7	6	wn 3	. . . . . 6 wff ¬ θ
8	5, 7	wi 4	. . . . 5 wff (¬ χ → ¬ θ)
9	3, 8	wi 4	. . . 4 wff ((φ → ψ) → (¬ χ → ¬ θ))
10	9, 4	wi 4	. . 3 wff (((φ → ψ) → (¬ χ → ¬ θ)) → χ)
11		wta	. . 3 wff τ
12	10, 11	wi 4	. 2 wff ((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ)
13	11, 1	wi 4	. . 3 wff (τ → φ)
14	6, 1	wi 4	. . 3 wff (θ → φ)
15	13, 14	wi 4	. 2 wff ((τ → φ) → (θ → φ))
16	12, 15	wi 4	1 wff (((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τ → φ) → (θ → φ)))

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