Theorem 19.37v 2096

Description: Version of 19.37 2275 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
19.37v	⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))

Distinct variable group:   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem 19.37v

Step	Hyp	Ref	Expression
1		19.35 1980	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
2		19.3v 2085	. . 3 ⊢ (∀𝑥𝜑 ↔ 𝜑)
3	2	imbi1i 341	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
4	1, 3	bitri 267	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 198  ∀wal 1654  ∃wex 1878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075

This theorem depends on definitions:  df-bi 199  df-ex 1879

This theorem is referenced by:  19.37ivOLD  2097  eqvincg  3547  axrep5  5002  fvn0ssdmfun  6604  kmlem14  9307  kmlem15  9308  bnj132  31337  bnj1098  31396  bnj150  31488  bnj865  31535  bnj996  31567  bnj1021  31576  bnj1090  31589  bnj1176  31615  bj-axrep5  33316  cnvssco  38752  refimssco  38753  19.37vv  39423  pm11.61  39432  relopabVD  39954  rmoanim  42002