Theorem exim 1828

Description: Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)

Assertion

Ref	Expression
exim	⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))

Proof of Theorem exim

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓))
2	1	aleximi 1826	1 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))

Syntax hints:   → wi 4  ∀wal 1531  ∃wex 1773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803

This theorem depends on definitions:  df-bi 206  df-ex 1774

This theorem is referenced by:  eximi  1829  19.38b  1835  19.23v  1937  alequexv  1996  nf5-1  2133  spimt  2379  darii  2653  festino  2662  baroco  2664  darapti  2672  elex2OLD  3485  elex22  3486  vtoclegftOLD  3570  spcimgft  3572  rspn0  4354  exel  5438  bj-axdd2  36245  bj-2exim  36264  bj-sylget  36273  bj-alexim  36279  bj-cbvalimt  36291  bj-cbveximt  36292  bj-eqs  36327  bj-nnf-exlim  36409  bj-nnflemee  36416  bj-nnflemae  36417  bj-axc10  36436  bj-alequex  36437  bj-spimtv  36447  bj-spcimdv  36549  bj-spcimdvv  36550  sn-exelALT  41883  nfa1w  42267  2exim  43990  pm11.71  44008  onfrALTlem2  44159  19.41rg  44163  ax6e2nd  44171  elex2VD  44451  elex22VD  44452  onfrALTlem2VD  44502  19.41rgVD  44515  ax6e2eqVD  44520  ax6e2ndVD  44521  ax6e2ndeqVD  44522  ax6e2ndALT  44543  ax6e2ndeqALT  44544