Theorem 19.37v 2027

Description: Version of 19.37 2268 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 1907	. 2 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓))
2		19.3v 2012	. . 3 ⊢ (∀𝑥𝜑 ↔ 𝜑)
3	2	imbi1i 352	. 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓))
4	1, 3	bitri 278	1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓))

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997

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

This theorem is referenced by:  spc3egv  3562  eqvincg  3607  rmoanim  3848  rmoanimALT  3849  axrep5  5246  fvn0ssdmfun  7069  kmlem14  10143  kmlem15  10144  bnj132  35115  bnj1098  35172  bnj150  35264  bnj865  35311  bnj996  35344  bnj1021  35354  bnj1090  35367  bnj1176  35393  sn-axrep5v  43008  cnvssco  44352  refimssco  44353  19.37vv  45115  pm11.61  45123  relopabVD  45629