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  1788  darii  2180  barbari  2182  festino  2186  baroco  2187  cesaro  2188  camestros  2189  datisi  2190  disamis  2191  felapton  2194  darapti  2195  dimatis  2197  fresison  2198  calemos  2199  fesapo  2200  bamalip  2201  ceqsexv2d  2844  vtoclf  2858  vtocl2  2860  vtocl3  2861  nalset  4224  el  4274  dtruarb  4287  snnex  4551  eusv2nf  4559  dtruex  4663  limom  4718  nninfct  12675  bj-axemptylem  16591  bj-nalset  16594  bj-d0clsepcl  16624  bj-omex2  16676  bj-nn0sucALT  16677