Theorem 19.41v 1914

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 1537	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
2	1	19.41h 1696	1 ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓))

Syntax hints:   ∧ wa 104   ↔ wb 105  ∃wex 1503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  19.41vv  1915  19.41vvv  1916  19.41vvvv  1917  exdistrv  1922  eeeanv  1945  gencbvex  2798  euxfrdc  2938  euind  2939  dfdif3  3260  r19.9rmv  3529  opabm  4298  eliunxp  4784  relop  4795  dmuni  4855  dmres  4946  dminss  5061  imainss  5062  ssrnres  5089  cnvresima  5136  resco  5151  rnco  5153  coass  5165  xpcom  5193  f11o  5513  fvelrnb  5584  rnoprab  5979  domen  6777  xpassen  6856  genpassl  7553  genpassu  7554