Theorem eximii 1626

Description: Inference associated with eximi 1624. (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 1624	. 2 ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
4	1, 3	ax-mp 5	1 ⊢ ∃𝑥𝜓

Syntax hints:   → wi 4  ∃wex 1516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  spimfv  1723  ax6evr  1729  spimed  1764  darii  2155  barbari  2157  festino  2161  baroco  2162  cesaro  2163  camestros  2164  datisi  2165  disamis  2166  felapton  2169  darapti  2170  dimatis  2172  fresison  2173  calemos  2174  fesapo  2175  bamalip  2176  ceqsexv2d  2814  vtoclf  2828  vtocl2  2830  vtocl3  2831  nalset  4182  el  4230  dtruarb  4243  snnex  4503  eusv2nf  4511  dtruex  4615  limom  4670  nninfct  12437  bj-axemptylem  15966  bj-nalset  15969  bj-d0clsepcl  15999  bj-omex2  16051  bj-nn0sucALT  16052