Theorem morimv 2252

Description: Move antecedent outside of "at most one." (Contributed by NM, 28-Jul-1995.)

Assertion

Ref	Expression
morimv	⊢ (∃*x(φ → ψ) → (φ → ∃*xψ))

Distinct variable group:   φ,x

Allowed substitution hint:   ψ(x)

Proof of Theorem morimv

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-1 6	. . . . . . 7 ⊢ (ψ → (φ → ψ))
2	1	a1i 10	. . . . . 6 ⊢ (φ → (ψ → (φ → ψ)))
3	2	imim1d 69	. . . . 5 ⊢ (φ → (((φ → ψ) → x = y) → (ψ → x = y)))
4	3	alimdv 1621	. . . 4 ⊢ (φ → (∀x((φ → ψ) → x = y) → ∀x(ψ → x = y)))
5	4	eximdv 1622	. . 3 ⊢ (φ → (∃y∀x((φ → ψ) → x = y) → ∃y∀x(ψ → x = y)))
6		nfv 1619	. . . 4 ⊢ Ⅎy(φ → ψ)
7	6	mo2 2233	. . 3 ⊢ (∃*x(φ → ψ) ↔ ∃y∀x((φ → ψ) → x = y))
8		nfv 1619	. . . 4 ⊢ Ⅎyψ
9	8	mo2 2233	. . 3 ⊢ (∃*xψ ↔ ∃y∀x(ψ → x = y))
10	5, 7, 9	3imtr4g 261	. 2 ⊢ (φ → (∃*x(φ → ψ) → ∃*xψ))
11	10	com12 27	1 ⊢ (∃*x(φ → ψ) → (φ → ∃*xψ))

This proof depends on syntax axioms:   → wi 4  ∀wal 1540  ∃wex 1541   = wceq 1642  ∃*wmo 2205

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This proof depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209

This theorem is used by: (None)