Theorem 19.22i 723

Description: Inference adding existential quantifier to antecedent and consequent.

Hypothesis

Ref	Expression
19.22i.1	⊢ (φ → ψ)

Assertion

Ref	Expression
19.22i	⊢ (∃xφ → ∃xψ)

Proof of Theorem 19.22i

Step	Hyp	Ref	Expression
1		19.22 722	. 2 ⊢ (∀x(φ → ψ) → (∃xφ → ∃xψ))
2		19.22i.1	. 2 ⊢ (φ → ψ)
3	1, 2	mpg 684	1 ⊢ (∃xφ → ∃xψ)

Syntax hints:   → wi 2  ∃wex 678

This theorem is referenced by:  excomim 727  19.12 729  19.23ai 746  19.40 773  eqvin.l1 851  sbimi 854  sbequi 876  mo 1020  eumo0 1022  eupickb 1056  mopick2 1057  moexex 1058  2euex 1061  2eu2ex 1063  2exeu 1066  rexex 1242  r19.22i2 1274  cgsex2g 1368  cgsex4g 1369  vtoclf 1377  vtocl2 1379  vtocl3 1380  cla4gf 1394  axrep 1473  zfaus 1480  bm1.3ii 1481  nalset 1482  zfnul 1746  mosubop 1911  euuni 1954  ssiun 2018  iununi 2037  ralxp 2456  xpss 2465  dmco 2570  dmcosseq 2572  imassrn 2611  dminss 2648  imainss 2649  zfrep6 2744  fv3 2839  abrexexlem1 2910  tz7.48-1 2994  ssoprab2i 3036  enssdom 3287  unblem2 3432  infcntss 3443  inf1 3458  inf5 3472  omex 3475  scott0 3542  bnd 3548  aceq3 3556  aceq4 3557  ac5b 3574  ac6 3576  ac6s 3577  ac6s2 3578  kmlem1 3580  kmlem2 3581  kmlem13 3592  cflim 3704  axpowndlem2 3744  axacndlem4 3756  prnmadd 3894  1idpr 3927  ltexprlem4 3939  reclem1pr 3950  reclem2pr 3951  recexpr 3954  suplem1pr 3955  suplem2pr 3956  recexsrlem 4006  suppsr2 4017  suppsr3 4018  axsup 4088  infxpidmlem8 4940  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-gen 677

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

metamath.org