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

Metamath Proof Explorer

Theorem poeq12d

Description: Equality deduction for partial orderings. (Contributed by Matthew House, 10-Sep-2025)

	Ref	Expression
Hypotheses	poeq12d.1	$⊢ φ \to R = S$
	poeq12d.2	$⊢ φ \to A = B$
Assertion	poeq12d	$⊢ φ \to (R Po A \leftrightarrow S Po B)$

Step	Hyp	Ref	Expression
1		poeq12d.1	$⊢ φ \to R = S$
2		poeq12d.2	$⊢ φ \to A = B$
3		poeq1	$⊢ R = S \to (R Po A \leftrightarrow S Po A)$
4		poeq2	$⊢ A = B \to (S Po A \leftrightarrow S Po B)$
5	3 4	sylan9bb	$⊢ (R = S \land A = B) \to (R Po A \leftrightarrow S Po B)$
6	1 2 5	syl2anc	$⊢ φ \to (R Po A \leftrightarrow S Po B)$