Theorem 19.42v 1905

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

Assertion

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

Distinct variable group:   φ,x

Allowed substitution hint:   ψ(x)

Proof of Theorem 19.42v

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 ⊢ Ⅎxφ
2	1	19.42 1880	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:  exdistr  1906  19.42vv  1907  19.42vvv  1908  4exdistr  1911  cbvex2  2005  2sb5  2112  2sb5rf  2117  rexcom4a  2880  ceqsex2  2896  reuind  3040  2reu5lem3  3044  sbccomlem  3117  elpw1  4145  eluni1g  4173  opkelopkabg  4246  otkelins2kg  4254  eqvinop  4607  setconslem6  4737  dmopabss  4917  dmopab3  4918  dmcosseq  4974  coass  5098  dmoprab  5575  dmoprabss  5576  fnoprabg  5586  mptpreima  5683  dmmpt  5684  brsnsi2  5777  oqelins4  5795  addcfnex  5825  lecex  6116  ceex  6175  nmembers1lem1  6269  dmfrec  6317