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

Theorem eximii 1761
Description: Inference associated with eximi 1759. (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 1759 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
41, 3ax-mp 5 1 𝑥𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  exiftru  1893  spimeh  1927  ax6evr  1944  spimv1  2117  cbv3hvOLD  2177  cbv3hvOLDOLD  2178  ax6e  2254  spim  2258  spimed  2259  spimv  2261  spei  2265  equvini  2350  equvel  2351  euequ1  2480  euex  2498  darii  2569  barbari  2571  festino  2575  baroco  2576  cesaro  2577  camestros  2578  datisi  2579  disamis  2580  felapton  2583  darapti  2584  dimatis  2586  fresison  2587  calemos  2588  fesapo  2589  bamalip  2590  vtoclf  3249  vtocl  3250  axrep2  4738  axnul  4753  nalset  4760  notzfaus  4805  el  4812  dtru  4822  eusv2nf  4829  dvdemo1  4868  dvdemo2  4869  axpr  4871  snnex  6918  inf1  8464  bnd  8700  axpowndlem2  9365  grothomex  9596  bnj101  30489  axextdfeq  31392  ax8dfeq  31393  axextndbi  31399  snelsingles  31644  bj-ax6elem2  32267  bj-spimedv  32334  bj-spimvv  32336  bj-speiv  32339  bj-axrep2  32405  bj-nalset  32410  bj-el  32412  bj-dtru  32413  bj-dvdemo1  32418  bj-dvdemo2  32419  ax6er  32436  bj-vtoclf  32528  wl-exeq  32929  spd  41672  elpglem2  41703  eximp-surprise2  41789
  Copyright terms: Public domain W3C validator