Theorem 19.41v 1841

Description: Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
19.41v	⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Distinct variable group:   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 19.41v

Step	Hyp	Ref	Expression
1		ax-17 1474	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
2	1	19.41h 1631	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ∧ wa 103   ↔ wb 104  ∃wex 1436

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  19.41vv  1842  19.41vvv  1843  19.41vvvv  1844  exdistrv  1847  eeeanv  1868  gencbvex  2687  euxfrdc  2823  euind  2824  dfdif3  3133  r19.9rmv  3401  opabm  4140  eliunxp  4616  relop  4627  dmuni  4687  dmres  4776  dminss  4889  imainss  4890  ssrnres  4917  cnvresima  4964  resco  4979  rnco  4981  coass  4993  xpcom  5021  f11o  5334  fvelrnb  5401  rnoprab  5786  domen  6575  xpassen  6653  genpassl  7233  genpassu  7234