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  1888  spimeh  1922  ax6evr  1939  spimv1  2112  cbv3hvOLD  2172  cbv3hvOLDOLD  2173  ax6e  2249  spim  2253  spimed  2254  spimv  2256  spei  2260  equvini  2345  equvel  2346  euequ1  2475  euex  2493  darii  2564  barbari  2566  festino  2570  baroco  2571  cesaro  2572  camestros  2573  datisi  2574  disamis  2575  felapton  2578  darapti  2579  dimatis  2581  fresison  2582  calemos  2583  fesapo  2584  bamalip  2585  vtoclf  3248  vtocl  3249  axrep2  4743  axnul  4758  nalset  4765  notzfaus  4810  el  4817  dtru  4827  eusv2nf  4834  dvdemo1  4873  dvdemo2  4874  axpr  4876  snnexOLD  6931  inf1  8479  bnd  8715  axpowndlem2  9380  grothomex  9611  bnj101  30550  axextdfeq  31457  ax8dfeq  31458  axextndbi  31464  snelsingles  31724  bj-ax6elem2  32347  bj-spimedv  32414  bj-spimvv  32416  bj-speiv  32419  bj-axrep2  32485  bj-nalset  32490  bj-el  32492  bj-dtru  32493  bj-dvdemo1  32498  bj-dvdemo2  32499  ax6er  32516  bj-vtoclf  32608  wl-exeq  32992  spd  41747  elpglem2  41778  eximp-surprise2  41864
  Copyright terms: Public domain W3C validator