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

Axiom ax-meredith 1396
Description: Theorem meredith 1394 restated as an axiom. This will allow us to ensure that the rederivation of ax1 1421, ax2 1422, and ax3 1423 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  1397  merlem2  1398  merlem3  1399  merlem4  1400  merlem5  1401  merlem7  1403  merlem8  1404  merlem9  1405  merlem10  1406  merlem11  1407  merlem13  1409  luk-1  1410  luk-2  1411
  Copyright terms: Public domain W3C validator