Theorem lemma-L7.02a-L1 943

Description: Lemma for lemma-L7.02a 944. †

Hypotheses

Ref	Expression
lemma-L7.02a-L1.1	⊢ Ⅎ𝑥𝛾
lemma-L7.02a-L1.2	⊢ (𝛾 → (𝜑 → 𝜓))

Assertion

Ref	Expression
lemma-L7.02a-L1	⊢ (𝛾 → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓))

Distinct variable group:   𝑡,𝑥

Proof of Theorem lemma-L7.02a-L1

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		lemma-L7.02a-L1.1	. 2 ⊢ Ⅎ𝑥𝛾
2		ndpsub3-P7.15 840	. . 3 ⊢ Ⅎ𝑥[𝑡 / 𝑥]𝜑
3		ndpsub3-P7.15 840	. . 3 ⊢ Ⅎ𝑥[𝑡 / 𝑥]𝜓
4	2, 3	ndnfrim-P7.3.RC 876	. 2 ⊢ Ⅎ𝑥([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)
5		ndpsub2-P7.14 839	. . . . . . . 8 ⊢ (𝑥 = 𝑡 → (𝜑 ↔ [𝑡 / 𝑥]𝜑))
6	5	ndbier-P3.15 180	. . . . . . 7 ⊢ (𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 → 𝜑))
7	6	rcp-NDIMP0addall 207	. . . . . 6 ⊢ (𝛾 → (𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 → 𝜑)))
8	7	import-P3.34a.RC 306	. . . . 5 ⊢ ((𝛾 ∧ 𝑥 = 𝑡) → ([𝑡 / 𝑥]𝜑 → 𝜑))
9		lemma-L7.02a-L1.2	. . . . . 6 ⊢ (𝛾 → (𝜑 → 𝜓))
10	9	rcp-NDIMP1add1 208	. . . . 5 ⊢ ((𝛾 ∧ 𝑥 = 𝑡) → (𝜑 → 𝜓))
11		ndpsub2-P7.14 839	. . . . . . . 8 ⊢ (𝑥 = 𝑡 → (𝜓 ↔ [𝑡 / 𝑥]𝜓))
12	11	ndbief-P3.14 179	. . . . . . 7 ⊢ (𝑥 = 𝑡 → (𝜓 → [𝑡 / 𝑥]𝜓))
13	12	rcp-NDIMP0addall 207	. . . . . 6 ⊢ (𝛾 → (𝑥 = 𝑡 → (𝜓 → [𝑡 / 𝑥]𝜓)))
14	13	import-P3.34a.RC 306	. . . . 5 ⊢ ((𝛾 ∧ 𝑥 = 𝑡) → (𝜓 → [𝑡 / 𝑥]𝜓))
15	8, 10, 14	dsyl-P3.25 261	. . . 4 ⊢ ((𝛾 ∧ 𝑥 = 𝑡) → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓))
16		lemma-L7.01a 924	. . . . . 6 ⊢ ([𝑥 / 𝑦] 𝑦 = 𝑡 ↔ 𝑥 = 𝑡)
17	16	bisym-P3.33b.RC 299	. . . . 5 ⊢ (𝑥 = 𝑡 ↔ [𝑥 / 𝑦] 𝑦 = 𝑡)
18	17	subandr-P3.42b.RC 342	. . . 4 ⊢ ((𝛾 ∧ 𝑥 = 𝑡) ↔ (𝛾 ∧ [𝑥 / 𝑦] 𝑦 = 𝑡))
19	15, 18	subiml2-P4.RC 541	. . 3 ⊢ ((𝛾 ∧ [𝑥 / 𝑦] 𝑦 = 𝑡) → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓))
20	19	rcp-NDIMI2 224	. 2 ⊢ (𝛾 → ([𝑥 / 𝑦] 𝑦 = 𝑡 → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓)))
21		axL6ex-P7 925	. . 3 ⊢ ∃𝑦 𝑦 = 𝑡
22	21	rcp-NDIMP0addall 207	. 2 ⊢ (𝛾 → ∃𝑦 𝑦 = 𝑡)
23	1, 4, 20, 22	ndexew-P7.VR2of3 869	1 ⊢ (𝛾 → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓))

Syntax hints:  term-obj 1   = wff-equals 6   → wff-imp 10   ∧ wff-and 132  ∃wff-exists 595  Ⅎwff-nfree 681  [wff-psub 714

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-L10 27  ax-L11 28  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  df-psub-D6.2 716

This theorem is referenced by:  lemma-L7.02a  944