Theorem 19.41v 1901

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

Assertion

Ref	Expression
19.41v	⊢ (∃x(φ ∧ ψ) ↔ (∃xφ ∧ ψ))

Distinct variable group:   ψ,x

Allowed substitution hint:   φ(x)

Proof of Theorem 19.41v

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 ⊢ Ⅎxψ
2	1	19.41 1879	1 ⊢ (∃x(φ ∧ ψ) ↔ (∃xφ ∧ ψ))

Syntax hints:   ↔ wb 176   ∧ wa 358  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545

This theorem is referenced by:  19.41vv  1902  19.41vvv  1903  19.41vvvv  1904  eeeanv  1914  gencbvex  2901  euxfr  3022  euind  3023  elpw11c  4147  elpw121c  4148  elpw131c  4149  elpw141c  4150  elpw151c  4151  elpw161c  4152  elpw171c  4153  elpw181c  4154  elpw191c  4155  elpw1101c  4156  elpw1111c  4157  eluni1g  4172  opkelcokg  4261  opkelimagekg  4271  dfimak2  4298  insklem  4304  ndisjrelk  4323  dfpw2  4327  dfaddc2  4381  dfnnc2  4395  elsuc  4413  nnsucelrlem1  4424  ltfinex  4464  ssfin  4470  eqpwrelk  4478  eqpw1relk  4479  ncfinraiselem2  4480  ncfinlowerlem1  4482  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  nnpweqlem1  4522  srelk  4524  sfintfinlem1  4531  tfinnnlem1  4533  spfinex  4537  vfinspsslem1  4550  dfop2lem1  4573  opeq  4619  opabn0  4716  setconslem1  4731  setconslem2  4732  setconslem3  4733  setconslem7  4737  df1st2  4738  dfswap2  4741  eliunxp  4821  dmuni  4914  elimapw11c  4948  dmres  4986  rnuni  5038  dminss  5041  imainss  5042  ssrnres  5059  cnvresima  5077  resco  5085  rnco  5087  coass  5097  df2nd2  5111  f11o  5315  dmsi  5519  rnoprab  5576  brimage  5793  dmtxp  5802  txpcofun  5803  addcfnex  5824  brpprod  5839  dmpprod  5840  pw1fnf1o  5855  fundmen  6043  ceexlem1  6173  el2c  6191  taddc  6229  tcfnex  6244  csucex  6259  addccan2nclem1  6263  nchoicelem11  6299  nchoicelem16  6304