Theorem eximii 1624

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

Syntax hints:   → wi 4  ∃wex 1514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-ial 1556

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  spimfv  1721  ax6evr  1727  spimed  1762  darii  2153  barbari  2155  festino  2159  baroco  2160  cesaro  2161  camestros  2162  datisi  2163  disamis  2164  felapton  2167  darapti  2168  dimatis  2170  fresison  2171  calemos  2172  fesapo  2173  bamalip  2174  ceqsexv2d  2811  vtoclf  2825  vtocl2  2827  vtocl3  2828  nalset  4173  el  4221  dtruarb  4234  snnex  4494  eusv2nf  4502  dtruex  4606  limom  4661  nninfct  12304  bj-axemptylem  15761  bj-nalset  15764  bj-d0clsepcl  15794  bj-omex2  15846  bj-nn0sucALT  15847