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

Metamath Proof Explorer

Theorem otth2

Description: Ordered triple theorem, with triple expressed with ordered pairs. (Contributed by NM, 1-May-1995) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Hypotheses otth.1 ⊢ A ∈ V
otth.2 ⊢ B ∈ V
otth.3 ⊢ R ∈ V
Assertion otth2 ⊢ A B R = C D S ↔ A = C ∧ B = D ∧ R = S

Proof

Step Hyp Ref Expression
1 otth.1 ⊢ A ∈ V
2 otth.2 ⊢ B ∈ V
3 otth.3 ⊢ R ∈ V
4 1 2 opth ⊢ A B = C D ↔ A = C ∧ B = D
5 4 anbi1i ⊢ A B = C D ∧ R = S ↔ A = C ∧ B = D ∧ R = S
6 opex ⊢ A B ∈ V
7 6 3 opth ⊢ A B R = C D S ↔ A B = C D ∧ R = S
8 df-3an ⊢ A = C ∧ B = D ∧ R = S ↔ A = C ∧ B = D ∧ R = S
9 5 7 8 3bitr4i ⊢ A B R = C D S ↔ A = C ∧ B = D ∧ R = S