Theorem 19.37v 1998

Description: Version of 19.37 2237 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 1878	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
2		19.3v 1983	. . 3 ⊢ (∀𝑥𝜑 ↔ 𝜑)
3	2	imbi1i 349	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
4	1, 3	bitri 275	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968

This theorem depends on definitions:  df-bi 207  df-ex 1781

This theorem is referenced by:  spc3egv  3555  eqvincg  3600  rmoanim  3842  rmoanimALT  3843  axrep5  5230  fvn0ssdmfun  7017  kmlem14  10072  kmlem15  10073  bnj132  34831  bnj1098  34888  bnj150  34981  bnj865  35028  bnj996  35061  bnj1021  35071  bnj1090  35084  bnj1176  35110  sn-axrep5v  42414  cnvssco  43789  refimssco  43790  19.37vv  44568  pm11.61  44576  relopabVD  45083