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

Axiom ax-meredith 1415
Description: Theorem meredith 1413 restated as an axiom. This will allow us to ensure that the rederivation of ax1 1440, ax2 1441, and ax3 1442 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  1416  merlem2  1417  merlem3  1418  merlem4  1419  merlem5  1420  merlem7  1422  merlem8  1423  merlem9  1424  merlem10  1425  merlem11  1426  merlem13  1428  luk-1  1429  luk-2  1430
  Copyright terms: Public domain W3C validator