Metamath Proof Explorer


Theorem opelxpii

Description: Ordered pair membership in a Cartesian product (implication). (Contributed by Steven Nguyen, 17-Jul-2022)

Ref Expression
Hypotheses opelxpii.1 A C
opelxpii.2 B D
Assertion opelxpii A B C × D

Proof

Step Hyp Ref Expression
1 opelxpii.1 A C
2 opelxpii.2 B D
3 opelxpi A C B D A B C × D
4 1 2 3 mp2an A B C × D