Theorem eximii 1650

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

Syntax hints:   → wi 4  ∃wex 1540

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-ial 1582

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  2843  vtoclf  2857  vtocl2  2859  vtocl3  2860  nalset  4219  el  4268  dtruarb  4281  snnex  4545  eusv2nf  4553  dtruex  4657  limom  4712  nninfct  12611  bj-axemptylem  16487  bj-nalset  16490  bj-d0clsepcl  16520  bj-omex2  16572  bj-nn0sucALT  16573