Theorem tbw-ax1 15114

Description: The first of four axioms in the Tarski-Bernays-Wajsberg system.

Assertion

Ref	Expression
tbw-ax1	|- ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))

Proof of Theorem tbw-ax1

Step	Hyp	Ref	Expression
1		imim1 58	1 |- ((ph -> ps) -> ((ps -> ch) -> (ph -> ch)))

Syntax hints:   -> wi 3

This theorem is referenced by:  tbwsyl 15118  tbwlem1 15119  tbwlem2 15120  tbwlem3 15121  tbwlem4 15122  tbwlem5 15123  re1luk1 15124  re1luk2 15125  re1luk3 15126

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain