Theorem 19.37v 1995

Description: Version of 19.37 2225 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 1880	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
2		19.3v 1985	. . 3 ⊢ (∀𝑥𝜑 ↔ 𝜑)
3	2	imbi1i 350	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
4	1, 3	bitri 274	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  spc3egv  3542  eqvincg  3578  rmoanim  3827  rmoanimALT  3828  axrep5  5215  fvn0ssdmfun  6952  kmlem14  9919  kmlem15  9920  bnj132  32705  bnj1098  32763  bnj150  32856  bnj865  32903  bnj996  32936  bnj1021  32946  bnj1090  32959  bnj1176  32985  sn-axrep5v  40185  cnvssco  41214  refimssco  41215  19.37vv  42003  pm11.61  42011  relopabVD  42521