Theorem eximii 1838

Description: Inference associated with eximi 1836. (Contributed by BJ, 3-Feb-2018.)

Hypotheses

Ref	Expression
eximii.1	⊢ ∃𝑥𝜑
eximii.2	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
eximii	⊢ ∃𝑥𝜓

Proof of Theorem eximii

Step	Hyp	Ref	Expression
1		eximii.1	. 2 ⊢ ∃𝑥𝜑
2		eximii.2	. . 3 ⊢ (𝜑 → 𝜓)
3	2	eximi 1836	. 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
4	1, 3	ax-mp 5	1 ⊢ ∃𝑥𝜓

Syntax hints:   → wi 4  ∃wex 1781

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

This theorem depends on definitions:  df-bi 210  df-ex 1782

This theorem is referenced by:  exan  1863  spimehOLD  1975  exgenOLD  1979  ax6evr  2022  spimedv  2195  spimfv  2239  ax6e  2390  spim  2394  spimed  2395  spimvALT  2398  spei  2401  equvini  2466  equviniOLD  2467  equvel  2468  euequ  2658  dariiALT  2728  barbariALT  2732  festinoALT  2737  barocoALT  2739  daraptiALT  2747  vtoclf  3506  axrep2  5157  axnul  5173  nalset  5181  notzfaus  5227  notzfausOLD  5228  el  5235  dtru  5236  dvdemo1  5239  dvdemo2  5240  eusv2nf  5261  axprALT  5288  axpr  5294  inf1  9069  bnd  9305  axpowndlem2  10009  grothomex  10240  tgjustc1  26269  tgjustc2  26270  bnj101  32103  axextdfeq  33155  ax8dfeq  33156  axextndbi  33162  snelsingles  33496  bj-ax6elem2  34113  bj-dtru  34254  ax6er  34271  bj-vtoclf  34355  wl-exeq  34939  sn-el  39402  spd  45208  elpglem2  45241  eximp-surprise2  45313