Theorem eximii 1602

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

Syntax hints:   → wi 4  ∃wex 1492

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  spimfv  1699  ax6evr  1705  spimed  1740  darii  2126  barbari  2128  festino  2132  baroco  2133  cesaro  2134  camestros  2135  datisi  2136  disamis  2137  felapton  2140  darapti  2141  dimatis  2143  fresison  2144  calemos  2145  fesapo  2146  bamalip  2147  vtoclf  2790  vtocl2  2792  vtocl3  2793  nalset  4132  el  4177  dtruarb  4190  snnex  4447  eusv2nf  4455  dtruex  4557  limom  4612  bj-axemptylem  14504  bj-nalset  14507  bj-d0clsepcl  14537  bj-omex2  14589  bj-nn0sucALT  14590