Theorem axmeredith 1405

Description: Alias for meredith 1404 which "verify markup *" will match to ax-meredith 1406. (Contributed by NM, 21-Aug-2017.) (New usage is discouraged.)

Assertion

Ref	Expression
axmeredith	|- (((((ph -> ps) -> (-. ch -> -. th)) -> ch) -> ta) -> ((ta -> ph) -> (th -> ph)))

Proof of Theorem axmeredith

Step	Hyp	Ref	Expression
1		meredith 1404	1 |- (((((ph -> ps) -> (-. ch -> -. th)) -> ch) -> ta) -> ((ta -> ph) -> (th -> ph)))

Syntax hints:  -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by: (None)