Metamath Proof Explorer


Theorem rexor

Description: Alias for r19.43 for easier lookup. (Contributed by SN, 5-Jul-2025) (New usage is discouraged.)

Ref Expression
Assertion rexor x A φ ψ x A φ x A ψ

Proof

Step Hyp Ref Expression
1 r19.43 x A φ ψ x A φ x A ψ