3optocl

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

	Ref	Expression
Hypotheses	3optocl.1	$⊢ R = D \times F$
	3optocl.2	$⊢ ⟨x, y⟩ = A \to (φ \leftrightarrow ψ)$
	3optocl.3	$⊢ ⟨z, w⟩ = B \to (ψ \leftrightarrow χ)$
	3optocl.4	$⊢ ⟨v, u⟩ = C \to (χ \leftrightarrow θ)$
	3optocl.5	$⊢ ((x \in D \land y \in F) \land (z \in D \land w \in F) \land (v \in D \land u \in F)) \to φ$
Assertion	3optocl	$⊢ (A \in R \land B \in R \land C \in R) \to θ$

Step	Hyp	Ref	Expression
1		3optocl.1	$⊢ R = D \times F$
2		3optocl.2	$⊢ ⟨x, y⟩ = A \to (φ \leftrightarrow ψ)$
3		3optocl.3	$⊢ ⟨z, w⟩ = B \to (ψ \leftrightarrow χ)$
4		3optocl.4	$⊢ ⟨v, u⟩ = C \to (χ \leftrightarrow θ)$
5		3optocl.5	$⊢ ((x \in D \land y \in F) \land (z \in D \land w \in F) \land (v \in D \land u \in F)) \to φ$
6	4	imbi2d	$⊢ ⟨v, u⟩ = C \to (((A \in R \land B \in R) \to χ) \leftrightarrow ((A \in R \land B \in R) \to θ))$
7	2	imbi2d	$⊢ ⟨x, y⟩ = A \to (((v \in D \land u \in F) \to φ) \leftrightarrow ((v \in D \land u \in F) \to ψ))$
8	3	imbi2d	$⊢ ⟨z, w⟩ = B \to (((v \in D \land u \in F) \to ψ) \leftrightarrow ((v \in D \land u \in F) \to χ))$
9	5	3expia	$⊢ ((x \in D \land y \in F) \land (z \in D \land w \in F)) \to ((v \in D \land u \in F) \to φ)$
10	1 7 8 9	2optocl	$⊢ (A \in R \land B \in R) \to ((v \in D \land u \in F) \to χ)$
11	10	com12	$⊢ (v \in D \land u \in F) \to ((A \in R \land B \in R) \to χ)$
12	1 6 11	optocl	$⊢ C \in R \to ((A \in R \land B \in R) \to θ)$
13	12	impcom	$⊢ ((A \in R \land B \in R) \land C \in R) \to θ$
14	13	3impa	$⊢ (A \in R \land B \in R \land C \in R) \to θ$

Metamath Proof Explorer