Theorem 3optocl

Description: Implicit substitution of classes for ordered pairs. (Contributed by NM, 12-Mar-1995)

	Ref	Expression
Hypotheses	3optocl.1	⊢ 𝑅 = ( 𝐷 × 𝐹 )
	3optocl.2	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	3optocl.3	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
	3optocl.4	⊢ ( ⟨ 𝑣 , 𝑢 ⟩ = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
	3optocl.5	⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐹 ) ∧ ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹 ) ) → 𝜑 )
Assertion	3optocl	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑅 ) → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		3optocl.1	⊢ 𝑅 = ( 𝐷 × 𝐹 )
2		3optocl.2	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3		3optocl.3	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
4		3optocl.4	⊢ ( ⟨ 𝑣 , 𝑢 ⟩ = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
5		3optocl.5	⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐹 ) ∧ ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹 ) ) → 𝜑 )
6	4	imbi2d	⊢ ( ⟨ 𝑣 , 𝑢 ⟩ = 𝐶 → ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) → 𝜒 ) ↔ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) → 𝜃 ) ) )
7	2	imbi2d	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 → ( ( ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹 ) → 𝜑 ) ↔ ( ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹 ) → 𝜓 ) ) )
8	3	imbi2d	⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = 𝐵 → ( ( ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹 ) → 𝜓 ) ↔ ( ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹 ) → 𝜒 ) ) )
9	5	3expia	⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐹 ) ∧ ( 𝑧 ∈ 𝐷 ∧ 𝑤 ∈ 𝐹 ) ) → ( ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹 ) → 𝜑 ) )
10	1 7 8 9	2optocl	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) → ( ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹 ) → 𝜒 ) )
11	10	com12	⊢ ( ( 𝑣 ∈ 𝐷 ∧ 𝑢 ∈ 𝐹 ) → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) → 𝜒 ) )
12	1 6 11	optocl	⊢ ( 𝐶 ∈ 𝑅 → ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) → 𝜃 ) )
13	12	impcom	⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ) ∧ 𝐶 ∈ 𝑅 ) → 𝜃 )
14	13	3impa	⊢ ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑅 ∧ 𝐶 ∈ 𝑅 ) → 𝜃 )