Theorem eximii 1581

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

Syntax hints:   → wi 4  ∃wex 1468

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax6evr  1681  spimed  1718  darii  2099  barbari  2101  festino  2105  baroco  2106  cesaro  2107  camestros  2108  datisi  2109  disamis  2110  felapton  2113  darapti  2114  dimatis  2116  fresison  2117  calemos  2118  fesapo  2119  bamalip  2120  vtoclf  2739  vtocl2  2741  vtocl3  2742  nalset  4058  el  4102  dtruarb  4115  snnex  4369  eusv2nf  4377  dtruex  4474  limom  4527  bj-axemptylem  13090  bj-nalset  13093  bj-d0clsepcl  13123  bj-omex2  13175  bj-nn0sucALT  13176