Theorem eximii 1595

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

Syntax hints:   → wi 4  ∃wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-ial 1527

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  spimfv  1692  ax6evr  1698  spimed  1733  darii  2119  barbari  2121  festino  2125  baroco  2126  cesaro  2127  camestros  2128  datisi  2129  disamis  2130  felapton  2133  darapti  2134  dimatis  2136  fresison  2137  calemos  2138  fesapo  2139  bamalip  2140  vtoclf  2783  vtocl2  2785  vtocl3  2786  nalset  4119  el  4164  dtruarb  4177  snnex  4433  eusv2nf  4441  dtruex  4543  limom  4598  bj-axemptylem  13927  bj-nalset  13930  bj-d0clsepcl  13960  bj-omex2  14012  bj-nn0sucALT  14013