Theorem 19.37v 1998

Description: Version of 19.37 2232 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 1986	. . 3 ⊢ (∀𝑥𝜑 ↔ 𝜑)
3	2	imbi1i 353	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
4	1, 3	bitri 278	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970

This theorem depends on definitions:  df-bi 210  df-ex 1782

This theorem is referenced by:  spc3egv  3552  eqvincg  3589  rmoanim  3823  rmoanimALT  3824  axrep5  5160  fvn0ssdmfun  6819  kmlem14  9574  kmlem15  9575  bnj132  32106  bnj1098  32165  bnj150  32258  bnj865  32305  bnj996  32338  bnj1021  32348  bnj1090  32361  bnj1176  32387  sn-axrep5v  39400  cnvssco  40306  refimssco  40307  19.37vv  41089  pm11.61  41097  relopabVD  41607