Theorem eximii 1539

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

Syntax hints:   → wi 4  ∃wex 1427

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-ial 1473

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax6evr  1639  spimed  1676  darii  2049  barbari  2051  festino  2055  baroco  2056  cesaro  2057  camestros  2058  datisi  2059  disamis  2060  felapton  2063  darapti  2064  dimatis  2066  fresison  2067  calemos  2068  fesapo  2069  bamalip  2070  vtoclf  2673  vtocl2  2675  vtocl3  2676  nalset  3975  el  4019  dtruarb  4032  snnex  4283  eusv2nf  4291  dtruex  4388  limom  4441  bj-axemptylem  12056  bj-nalset  12059  bj-d0clsepcl  12093  bj-omex2  12145  bj-nn0sucALT  12146