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

Metamath Proof Explorer

Theorem pm1.2

Description: Axiom *1.2 of WhiteheadRussell p. 96, which they call "Taut". (Contributed by NM, 3-Jan-2005)

		Ref	Expression
	Assertion	pm1.2	$⊢ (φ \lor φ) \to φ$

Step	Hyp	Ref	Expression
1		id	$⊢ φ \to φ$
2	1 1	jaoi	$⊢ (φ \lor φ) \to φ$