MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-meredith Unicode version

Axiom ax-meredith 1412
Description: Theorem meredith 1410 restated as an axiom. This will allow us to ensure that the rederivation of ax1 1437, ax2 1438, and ax3 1439 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.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ax-meredith  |-  ( ( ( ( ( ph  ->  ps )  ->  ( -.  ch  ->  -.  th )
)  ->  ch )  ->  ta )  ->  (
( ta  ->  ph )  ->  ( th  ->  ph )
) )

Detailed syntax breakdown of Axiom ax-meredith
StepHypRef Expression
1 wph . . . . . 6  wff  ph
2 wps . . . . . 6  wff  ps
31, 2wi 4 . . . . 5  wff  ( ph  ->  ps )
4 wch . . . . . . 7  wff  ch
54wn 3 . . . . . 6  wff  -.  ch
6 wth . . . . . . 7  wff  th
76wn 3 . . . . . 6  wff  -.  th
85, 7wi 4 . . . . 5  wff  ( -. 
ch  ->  -.  th )
93, 8wi 4 . . . 4  wff  ( (
ph  ->  ps )  -> 
( -.  ch  ->  -. 
th ) )
109, 4wi 4 . . 3  wff  ( ( ( ph  ->  ps )  ->  ( -.  ch  ->  -.  th ) )  ->  ch )
11 wta . . 3  wff  ta
1210, 11wi 4 . 2  wff  ( ( ( ( ph  ->  ps )  ->  ( -.  ch  ->  -.  th )
)  ->  ch )  ->  ta )
1311, 1wi 4 . . 3  wff  ( ta 
->  ph )
146, 1wi 4 . . 3  wff  ( th 
->  ph )
1513, 14wi 4 . 2  wff  ( ( ta  ->  ph )  -> 
( th  ->  ph )
)
1612, 15wi 4 1  wff  ( ( ( ( ( ph  ->  ps )  ->  ( -.  ch  ->  -.  th )
)  ->  ch )  ->  ta )  ->  (
( ta  ->  ph )  ->  ( th  ->  ph )
) )
Colors of variables: wff set class
This axiom is referenced by:  merlem1  1413  merlem2  1414  merlem3  1415  merlem4  1416  merlem5  1417  merlem7  1419  merlem8  1420  merlem9  1421  merlem10  1422  merlem11  1423  merlem13  1425  luk-1  1426  luk-2  1427
  Copyright terms: Public domain W3C validator