Theorem ddelimdf 909

Description: Deduction form of ddelimf 908. This version may be useful if we want to avoid ax-17 925 and use ax-16 922 instead.

Hypotheses

Ref	Expression
ddelimdf.1	⊢ (φ → ∀xφ)
ddelimdf.2	⊢ (φ → ∀zφ)
ddelimdf.3	⊢ (φ → (ψ → ∀xψ))
ddelimdf.4	⊢ (φ → (χ → ∀zχ))
ddelimdf.5	⊢ (φ → (z = y → (ψ ↔ χ)))

Assertion

Ref	Expression
ddelimdf	⊢ (φ → (¬ ∀x x = y → (χ → ∀xχ)))

Proof of Theorem ddelimdf

Step	Hyp	Ref	Expression
1		ddelimdf.2	. . . . . 6 ⊢ (φ → ∀zφ)
2		ddelimdf.1	. . . . . 6 ⊢ (φ → ∀xφ)
3	1, 2	19.21ai 740	. . . . 5 ⊢ (φ → ∀z∀xφ)
4		ddelimdf.3	. . . . . . 7 ⊢ (φ → (ψ → ∀xψ))
5	4	19.20i 691	. . . . . 6 ⊢ (∀xφ → ∀x(ψ → ∀xψ))
6	5	19.20i 691	. . . . 5 ⊢ (∀z∀xφ → ∀z∀x(ψ → ∀xψ))
7		hbsb4t 906	. . . . 5 ⊢ (∀z∀x(ψ → ∀xψ) → (¬ ∀x x = y → ([y / z]ψ → ∀x[y / z]ψ)))
8	3, 6, 7	3syl 21	. . . 4 ⊢ (φ → (¬ ∀x x = y → ([y / z]ψ → ∀x[y / z]ψ)))
9	8	imp 277	. . 3 ⊢ ((φ ∧ ¬ ∀x x = y) → ([y / z]ψ → ∀x[y / z]ψ))
10		ddelimdf.4	. . . . 5 ⊢ (φ → (χ → ∀zχ))
11		ddelimdf.5	. . . . 5 ⊢ (φ → (z = y → (ψ ↔ χ)))
12	1, 10, 11	sbied 903	. . . 4 ⊢ (φ → ([y / z]ψ ↔ χ))
13	12	adantr 306	. . 3 ⊢ ((φ ∧ ¬ ∀x x = y) → ([y / z]ψ ↔ χ))
14	2, 12	biald 782	. . . 4 ⊢ (φ → (∀x[y / z]ψ ↔ ∀xχ))
15	14	adantr 306	. . 3 ⊢ ((φ ∧ ¬ ∀x x = y) → (∀x[y / z]ψ ↔ ∀xχ))
16	9, 13, 15	3imtr3d 420	. 2 ⊢ ((φ ∧ ¬ ∀x x = y) → (χ → ∀xχ))
17	16	exp 291	1 ⊢ (φ → (¬ ∀x x = y → (χ → ∀xχ)))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672   = weq 797  [wsb 852

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853

metamath.org