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  2792  vtocl2  2794  vtocl3  2795  nalset  4135  el  4180  dtruarb  4193  snnex  4450  eusv2nf  4458  dtruex  4560  limom  4615  bj-axemptylem  14683  bj-nalset  14686  bj-d0clsepcl  14716  bj-omex2  14768  bj-nn0sucALT  14769