This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tb-ax2

Description: The second of three axioms in the Tarski-Bernays axiom system. (Contributed by Anthony Hart, 16-Aug-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	tb-ax2	$⊢ φ \to (ψ \to φ)$

Proof

Step	Hyp	Ref	Expression
1		ax-1	$⊢ φ \to (ψ \to φ)$