MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eximii Structured version   Visualization version   GIF version

Theorem eximii 1839
Description: Inference associated with eximi 1837. (Contributed by BJ, 3-Feb-2018.)
Hypotheses
Ref Expression
eximii.1 𝑥𝜑
eximii.2 (𝜑𝜓)
Assertion
Ref Expression
eximii 𝑥𝜓

Proof of Theorem eximii
StepHypRef Expression
1 eximii.1 . 2 𝑥𝜑
2 eximii.2 . . 3 (𝜑𝜓)
32eximi 1837 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
41, 3ax-mp 5 1 𝑥𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  exan  1865  ax6evr  2018  spimedv  2190  spimfv  2232  ax6e  2383  spim  2387  spimed  2388  spimvALT  2391  spei  2394  equvini  2455  equvel  2456  euequ  2597  dariiALT  2667  barbariALT  2671  festinoALT  2676  barocoALT  2678  daraptiALT  2686  vtoclf  3497  axrep2  5212  axnul  5229  nalset  5237  notzfaus  5285  elALT2  5292  dtruALT2  5293  dvdemo1  5296  dvdemo2  5297  eusv2nf  5318  axprALT  5345  axpr  5351  dtru  5359  inf1  9380  bnd  9650  axpowndlem2  10354  grothomex  10585  tgjustc1  26836  tgjustc2  26837  bnj101  32702  axextdfeq  33773  ax8dfeq  33774  axextndbi  33780  snelsingles  34224  bj-ax6elem2  34848  bj-dtru  34999  ax6er  35016  bj-vtoclf  35100  wl-exeq  35693  sn-el  40187  spd  46384  elpglem2  46417  eximp-surprise2  46489
  Copyright terms: Public domain W3C validator