Theorem trnsvsub-P6 763

Description: Strengthened Form of trnsvsubw-P6 710.

'𝑦' cannot occur in '𝑡'.

Hypotheses

Ref	Expression
trnsvsub-P6.1	⊢ Ⅎ𝑦𝜑
trnsvsub-P6.2	⊢ Ⅎ𝑦𝜒
trnsvsub-P6.3	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
trnsvsub-P6.4	⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
trnsvsub-P6	⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜒))

Distinct variable groups:   𝑡,𝑦   𝑥,𝑦

Proof of Theorem trnsvsub-P6

Step	Hyp	Ref	Expression
1		eqmiddle-P6.CL 709	. 2 ⊢ (𝑥 = 𝑡 → ∃𝑦(𝑥 = 𝑦 ∧ 𝑦 = 𝑡))
2		trnsvsub-P6.3	. . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3		trnsvsub-P6.4	. . . . 5 ⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒))
4	2, 3	joinimandres2-P4.RC 581	. . . 4 ⊢ ((𝑥 = 𝑦 ∧ 𝑦 = 𝑡) → ((𝜑 ↔ 𝜓) ∧ (𝜓 ↔ 𝜒)))
5		bitrns-P3.33c.CL 304	. . . 4 ⊢ (((𝜑 ↔ 𝜓) ∧ (𝜓 ↔ 𝜒)) → (𝜑 ↔ 𝜒))
6	4, 5	syl-P3.24.RC 260	. . 3 ⊢ ((𝑥 = 𝑦 ∧ 𝑦 = 𝑡) → (𝜑 ↔ 𝜒))
7	6	alloverimex-P5.RC.GEN 603	. 2 ⊢ (∃𝑦(𝑥 = 𝑦 ∧ 𝑦 = 𝑡) → ∃𝑦(𝜑 ↔ 𝜒))
8		trnsvsub-P6.1	. . . 4 ⊢ Ⅎ𝑦𝜑
9		trnsvsub-P6.2	. . . 4 ⊢ Ⅎ𝑦𝜒
10	8, 9	nfrbi-P6 691	. . 3 ⊢ Ⅎ𝑦(𝜑 ↔ 𝜒)
11	10	nfrexgen-P6 735	. 2 ⊢ (∃𝑦(𝜑 ↔ 𝜒) → (𝜑 ↔ 𝜒))
12	1, 7, 11	dsyl-P3.25.RC 262	1 ⊢ (𝑥 = 𝑡 → (𝜑 ↔ 𝜒))

Syntax hints:  term-obj 1   = wff-equals 6   → wff-imp 10   ↔ wff-bi 104   ∧ wff-and 132  ∃wff-exists 595  Ⅎwff-nfree 681

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14  ax-GEN 15  ax-L4 16  ax-L5 17  ax-L6 18  ax-L7 19  ax-L12 29

This theorem depends on definitions:  df-bi-D2.1 107  df-and-D2.2 133  df-or-D2.3 145  df-true-D2.4 155  df-rcp-AND3 161  df-exists-D5.1 596  df-nfree-D6.1 682

This theorem is referenced by:  lemma-L6.05a  764