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  2183  barbari  2185  festino  2189  baroco  2190  cesaro  2191  camestros  2192  datisi  2193  disamis  2194  felapton  2197  darapti  2198  dimatis  2200  fresison  2201  calemos  2202  fesapo  2203  bamalip  2204  ceqsexv2d  2856  vtoclf  2870  vtocl2  2872  vtocl3  2873  nalset  4245  el  4296  dtruarb  4309  snnex  4574  eusv2nf  4582  dtruex  4686  limom  4741  nninfct  12762  bj-axemptylem  16788  bj-nalset  16791  bj-d0clsepcl  16821  bj-omex2  16873  bj-nn0sucALT  16874