Theorem eximii 1616

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

Syntax hints:   → wi 4  ∃wex 1506

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  spimfv  1713  ax6evr  1719  spimed  1754  darii  2145  barbari  2147  festino  2151  baroco  2152  cesaro  2153  camestros  2154  datisi  2155  disamis  2156  felapton  2159  darapti  2160  dimatis  2162  fresison  2163  calemos  2164  fesapo  2165  bamalip  2166  ceqsexv2d  2803  vtoclf  2817  vtocl2  2819  vtocl3  2820  nalset  4164  el  4212  dtruarb  4225  snnex  4484  eusv2nf  4492  dtruex  4596  limom  4651  nninfct  12233  bj-axemptylem  15622  bj-nalset  15625  bj-d0clsepcl  15655  bj-omex2  15707  bj-nn0sucALT  15708