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 ⊢ ∃𝑥𝜓

Syntax hints:   → wi 4  ∃wex 1545

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This theorem depends on definitions:  df-bi 117

This theorem is referenced 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  4258  el  4310  dtruarb  4323  uniex2  4576  snnex  4589  eusv2nf  4597  dtruex  4701  limom  4756  nninfct  12796  bj-axemptylem  16832  bj-nalset  16835  bj-d0clsepcl  16865  bj-omex2  16917  bj-nn0sucALT  16918