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

Theorem eximii 1840
Description: Inference associated with eximi 1838. (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 1838 . 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  1866  ax6evr  2019  spimedv  2191  spimfv  2233  ax6e  2383  spim  2387  spimed  2388  spimvALT  2391  spei  2394  equvini  2455  equvel  2456  euequ  2592  dariiALT  2662  barbariALT  2666  festinoALT  2671  barocoALT  2673  daraptiALT  2681  vtoclfOLD  3547  axrep2  5284  axnul  5301  nalset  5309  notzfaus  5357  elALT2  5363  dtruALT2  5364  dvdemo1  5367  dvdemo2  5368  eusv2nf  5389  axprALT  5416  axpr  5422  exel  5429  dtruOLD  5437  inf1  9604  bnd  9874  axpowndlem2  10580  grothomex  10811  tgjustc1  27693  tgjustc2  27694  bnj101  33665  axextdfeq  34700  ax8dfeq  34701  axextndbi  34707  snelsingles  34825  bj-ax6elem2  35449  ax6er  35616  bj-vtoclf  35700  wl-exeq  36308  sn-exelALT  40951  spd  47563  elpglem2  47597  eximp-surprise2  47672
  Copyright terms: Public domain W3C validator