Theorem 19.23aiv 1297

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:   ψ,x

Proof of Theorem 19.23aiv

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

Syntax hints:   → wi 3  ∃wex 982

This theorem is referenced by:  19.23aivv 1298  mo 1395  mopick 1435  zfext2 1464  gencl 1831  cgsexg 1834  gencbvex2 1842  vtocleg 1858  eqvinc 1886  uniiunlem 2135  eluni 2510  axsep2 2709  bm1.3ii 2711  intex 2734  unipw 2762  moabex 2772  nnullss 2774  exss 2775  mosubopt 2810  ssopab2 2828  reuunisn 2901  limuni3 3129  findsg 3163  tfindsg 3168  relop 3281  dmrnssfld 3363  elxp5 3460  unixp0 3524  ffoss 3717  fvopabn 3792  exfo 3828  tfrlem8 3924  tfrlem9 3925  fnoprabg 4018  erref 4281  ectocl 4308  ecoptocl 4309  mapprc 4332  map0b 4349  map0 4350  uniixp 4363  breng 4381  brdomg 4382  ener 4416  en0 4429  en1 4432  2dom 4433  undom 4444  xpdom2 4448  xpdom3 4451  pw2en 4452  mapen 4497  mapdom1 4498  mapdom2 4500  ssenen 4510  php 4519  0sdom1dom 4530  unfilem1 4560  unifiOLD 4570  fodomfi 4575  fodomfiOLD 4576  pm54.43 4581  inf3 4629  infeq5 4630  omex 4636  zfregs 4657  tz9.12lem1 4669  bnd2 4734  aceq3lem 4742  aceq4 4744  aceq5lem4 4748  aceq5lem5 4749  aceq5 4750  aceq6a 4751  aceq6b 4752  ac6lem 4764  ac6s 4766  kmlem2 4776  kmlem16 4790  numthlem 4793  weth 4797  brdom3 4811  brdom5 4812  brdom4 4813  brdom7disj 4814  brdom6disj 4815  unidom 4818  oncard 4839  carduni 4869  cardcf 4923  cfeq0 4926  cfsuc 4927  cfom 4928  ltbtwnpq 5096  ltaprlem 5162  reclem1pr 5168  reclem2pr 5169  reclem3pr 5170  map2psrpr 5232  supsrlem2 5238  suprelem 5271  renegcl 5428  0re 5452  redivcl 5800  nnunb 6072  isumshft 7204  isumshft2 7205  acdc3 7488  acdc2 7491  acdc5 7494  acdc 7496  infxpidmlem4 7556  infxpidmlem7 7559  infxpidmlem10 7562  infxpidmlem12 7564  infpss 7575  infmap2lem2 7582  tgval3t 7624  eltg3t 7625  bastop 7641  isgrp2i 8072  minvecex 8574  projlem 9212  shintcl 9288  pjrn 9642  strlem1 10172  uninqs 10436  infi1 10441  fine 10442  fiiu 10444  ficli 10462  fiv 10470  fiiu2 10473  inposet 10477  homcard 10525  fisub 10558  infi 10559  rcfpfillem2 10564  rcfpfillem3 10565  rcfpfillem4 10566  rcfpfillem6 10568  rcfpfil 10569

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983

Copyright terms: Public domain