Theorem eximii 1533

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

Syntax hints:   → wi 4  ∃wex 1421

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-ial 1467

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  spimed  1668  darii  2041  barbari  2043  festino  2047  baroco  2048  cesaro  2049  camestros  2050  datisi  2051  disamis  2052  felapton  2055  darapti  2056  dimatis  2058  fresison  2059  calemos  2060  fesapo  2061  bamalip  2062  vtoclf  2652  vtocl2  2654  vtocl3  2655  nalset  3908  el  3952  dtruarb  3962  snnex  4199  eusv2nf  4206  dtruex  4302  limom  4354  bj-axemptylem  10683  bj-nalset  10686  bj-d0clsepcl  10720  bj-omex2  10772  bj-nn0sucALT  10773