Theorem 19.37v 1987

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1531  ∃wex 1773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963

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

This theorem is referenced by:  spc3egv  3592  eqvincg  3636  rmoanim  3889  rmoanimALT  3890  axrep5  5295  fvn0ssdmfun  7089  kmlem14  10194  kmlem15  10195  bnj132  34390  bnj1098  34447  bnj150  34540  bnj865  34587  bnj996  34620  bnj1021  34630  bnj1090  34643  bnj1176  34669  sn-axrep5v  41735  cnvssco  43067  refimssco  43068  19.37vv  43853  pm11.61  43861  relopabVD  44371