Theorem 19.37v 2017

Description: Version of 19.37 2267 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 1897	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
2		19.3v 2002	. . 3 ⊢ (∀𝑥𝜑 ↔ 𝜑)
3	2	imbi1i 351	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
4	1, 3	bitri 277	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1558  ∃wex 1799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987

This theorem depends on definitions:  df-bi 209  df-ex 1800

This theorem is referenced by:  spc3egv  3562  eqvincg  3607  rmoanim  3847  rmoanimALT  3848  axrep5  5235  fvn0ssdmfun  7055  kmlem14  10120  kmlem15  10121  bnj132  35022  bnj1098  35079  bnj150  35171  bnj865  35218  bnj996  35251  bnj1021  35261  bnj1090  35274  bnj1176  35300  sn-axrep5v  42836  cnvssco  44182  refimssco  44183  19.37vv  44961  pm11.61  44969  relopabVD  45476