Metamath Proof Explorer


Theorem otelxp

Description: Ordered triple membership in a triple Cartesian product. (Contributed by Scott Fenton, 31-Jan-2025)

Ref Expression
Assertion otelxp A B C D × E × F A D B E C F

Proof

Step Hyp Ref Expression
1 opelxp A B C D × E × F A B D × E C F
2 opelxp A B D × E A D B E
3 1 2 bianbi A B C D × E × F A D B E C F
4 df-ot A B C = A B C
5 4 eleq1i A B C D × E × F A B C D × E × F
6 df-3an A D B E C F A D B E C F
7 3 5 6 3bitr4i A B C D × E × F A D B E C F