Theorem eximii 1651

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

Syntax hints:   → wi 4  ∃wex 1541

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  spimfv  1747  ax6evr  1753  spimed  1789  darii  2181  barbari  2183  festino  2187  baroco  2188  cesaro  2189  camestros  2190  datisi  2191  disamis  2192  felapton  2195  darapti  2196  dimatis  2198  fresison  2199  calemos  2200  fesapo  2201  bamalip  2202  ceqsexv2d  2854  vtoclf  2868  vtocl2  2870  vtocl3  2871  nalset  4240  el  4291  dtruarb  4304  snnex  4569  eusv2nf  4577  dtruex  4681  limom  4736  nninfct  12737  bj-axemptylem  16662  bj-nalset  16665  bj-d0clsepcl  16695  bj-omex2  16747  bj-nn0sucALT  16748