Metamath Proof Explorer

Theorem ot2elxp

Description: Ordered triple membership in a triple cross product. (Contributed by Scott Fenton, 21-Aug-2024)

Ref Expression
Assertion ot2elxp ⊢ A B C ∈ D × E × F ↔ A ∈ D ∧ B ∈ E ∧ C ∈ F

Proof

Step Hyp Ref Expression
1 opelxp ⊢ A B ∈ D × E ↔ A ∈ D ∧ B ∈ E
2 1 anbi1i ⊢ A B ∈ D × E ∧ C ∈ F ↔ A ∈ D ∧ B ∈ E ∧ C ∈ F
3 opelxp ⊢ A B C ∈ D × E × F ↔ A B ∈ D × E ∧ C ∈ F
4 df-3an ⊢ A ∈ D ∧ B ∈ E ∧ C ∈ F ↔ A ∈ D ∧ B ∈ E ∧ C ∈ F
5 2 3 4 3bitr4i ⊢ A B C ∈ D × E × F ↔ A ∈ D ∧ B ∈ E ∧ C ∈ F