Theorem 19.23aiv 952

Description: Inference from Theorem 19.23 of [Margaris] p. 90.

Hypothesis

Ref	Expression
19.23aiv.1	⊢ (φ → ψ)

Assertion

Ref	Expression
19.23aiv	⊢ (∃xφ → ψ)

Distinct variable group(s):   ψ,x

Proof of Theorem 19.23aiv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 ⊢ (ψ → ∀xψ)
2		19.23aiv.1	. 2 ⊢ (φ → ψ)
3	1, 2	19.23ai 746	1 ⊢ (∃xφ → ψ)

Syntax hints:   → wi 2  ∃wex 678

This theorem is referenced by:  19.23aivv 953  mo 1020  mopick 1054  zfext2 1087  gencl 1365  vtocleg 1390  eqvinc 1407  sbcie 1455  bm1.3ii 1481  moabex 1868  nnullss 1880  exss 1881  mosubop 1911  eluni 1922  unipw 1960  intex 1986  ssopab2 2119  findsg 2398  tfindsg 2402  dmexg 2551  rnexg 2569  elxp5 2641  ffoss 2820  fvopabn 2873  tfrlem8 2956  tfrlem9 2957  fnoprab 3038  erref 3212  ectocl 3238  ecoptocl 3239  mapprc 3260  map0b 3267  map0 3268  breng 3280  brdomg 3281  ener 3313  en0 3328  en1 3331  2dom 3332  undom 3342  xpdom2 3345  xpdom3 3347  pw2en 3348  mapen 3386  mapdom1 3387  mapdom2 3389  ssenen 3399  php 3409  0sdom1dom 3420  unfilem1 3438  inf3 3471  inf5 3472  omex 3475  zfregs 3491  tz9.12lem1 3503  bnd2 3549  aceq3lem 3555  aceq4 3557  aceq5lem4 3561  aceq5lem5 3562  aceq5 3563  aceq6a 3564  aceq6b 3565  ac6lem 3575  ac6s 3577  kmlem2 3581  kmlem16 3595  numthlem 3598  weth 3602  fodomb 3615  oncard 3636  carduni 3664  cardcf 3706  cfsuc 3709  cfom 3710  ltbtwnpq 3878  ltaprlem 3944  reclem1pr 3950  reclem2pr 3951  reclem3pr 3952  map2psrpr 4014  supsrlem2 4020  suprelem 4053  renegcl 4171  redivcl 4274  nnunb 4520  infxpidmlem4 4936  infxpidmlem7 4939  infxpidmlem10 4942  infxpidmlem12 4944  infmap2lem2 4952  projlem 5224  shintcl 5294  pjrn 5587  strlem1 5691

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-an 198  df-ex 679

metamath.org