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

Metamath Proof Explorer

Theorem sbor2

Description: One direction of sbor , using fewer axioms. Compare 19.33 . (Contributed by Steven Nguyen, 18-Aug-2023)

		Ref	Expression
	Assertion	sbor2	$⊢ ([t/ x] φ \lor [t/ x] ψ) \to [t/ x] (φ \lor ψ)$

Step	Hyp	Ref	Expression
1		orc	$⊢ φ \to (φ \lor ψ)$
2	1	sbimi	$⊢ [t/ x] φ \to [t/ x] (φ \lor ψ)$
3		olc	$⊢ ψ \to (φ \lor ψ)$
4	3	sbimi	$⊢ [t/ x] ψ \to [t/ x] (φ \lor ψ)$
5	2 4	jaoi	$⊢ ([t/ x] φ \lor [t/ x] ψ) \to [t/ x] (φ \lor ψ)$