Theorem eximii 1582

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

Syntax hints:   → wi 4  ∃wex 1472

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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  spimfv  1679  ax6evr  1685  spimed  1720  darii  2106  barbari  2108  festino  2112  baroco  2113  cesaro  2114  camestros  2115  datisi  2116  disamis  2117  felapton  2120  darapti  2121  dimatis  2123  fresison  2124  calemos  2125  fesapo  2126  bamalip  2127  vtoclf  2765  vtocl2  2767  vtocl3  2768  nalset  4094  el  4138  dtruarb  4151  snnex  4406  eusv2nf  4414  dtruex  4516  limom  4571  bj-axemptylem  13426  bj-nalset  13429  bj-d0clsepcl  13459  bj-omex2  13511  bj-nn0sucALT  13512