Theorem 19.42v 966

Description: Special case of Theorem 19.42 of [Margaris] p. 90.

Assertion

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

Distinct variable group(s):   φ,x

Proof of Theorem 19.42v

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 ⊢ (φ → ∀xφ)
2	1	19.42 775	1 ⊢ (∃x(φ ∧ ψ) ↔ (φ ∧ ∃xψ))

Syntax hints:   ↔ wb 127   ∧ wa 196  ∃wex 678

This theorem is referenced by:  exdistr 967  19.42vv 968  3exdistr 970  4exdistr 971  euanv 1053  r2ex 1241  bm1.3ii 1481  eqvinop 1901  copsexg 1902  dfiun2 2014  opelxp 2452  dmopabss 2540  dmopab2 2541  dmsnop 2547  dmco 2570  dmcosseq 2572  coass 2667  dmco2 2673  zfrep6 2744  iinon 2948  dfoprab2 3021  dmoprab 3031  dmoprabss 3032  fnoprab 3038  aceq1 3552  aceq3 3556  ac5b 3574  kmlem14 3593  kmlem15 3594  genpdm 3899  genpn0 3900  distrlem1pr 3921  1idpr 3927  prlem934 3933  ltexprlem1 3936  ltexprlem4 3939  infmap2lem1 4951  osumlem5 5534

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679

metamath.org