Theorem eximii 1655

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This proof depends on definitions:  df-bi 117

This theorem is used by:  spimfv  1751  ax6evr  1757  spimed  1793  darii  2187  barbari  2189  festino  2193  baroco  2194  cesaro  2195  camestros  2196  datisi  2197  disamis  2198  felapton  2201  darapti  2202  dimatis  2204  fresison  2205  calemos  2206  fesapo  2207  bamalip  2208  ceqsexv2d  2862  vtoclf  2876  vtocl2  2878  vtocl3  2879  nalset  4263  el  4315  dtruarb  4328  uniex2  4581  snnex  4594  eusv2nf  4602  dtruex  4706  limom  4761  nninfct  12818  bj-axemptylem  16918  bj-nalset  16921  bj-d0clsepcl  16951  bj-omex2  17003  bj-nn0sucALT  17004