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

Theorem eximii 1804
Description: Inference associated with eximi 1802. (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 1802 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
41, 3ax-mp 5 1 𝑥𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-ex 1745
This theorem is referenced by:  exiftru  1948  spimeh  1971  ax6evr  1988  spimv1  2153  ax6e  2286  spim  2290  spimed  2291  spimv  2293  spei  2297  equvini  2374  equvel  2375  euequ1  2504  euex  2522  darii  2594  barbari  2596  festino  2600  baroco  2601  cesaro  2602  camestros  2603  datisi  2604  disamis  2605  felapton  2608  darapti  2609  dimatis  2611  fresison  2612  calemos  2613  fesapo  2614  bamalip  2615  vtoclf  3289  vtocl  3290  axrep2  4806  axnul  4821  nalset  4828  notzfaus  4870  el  4877  dtru  4887  eusv2nf  4894  dvdemo1  4932  dvdemo2  4933  axpr  4935  snnexOLD  7009  inf1  8557  bnd  8793  axpowndlem2  9458  grothomex  9689  bnj101  30917  axextdfeq  31827  ax8dfeq  31828  axextndbi  31834  snelsingles  32154  bj-ax6elem2  32777  bj-spimedv  32844  bj-spimvv  32846  bj-speiv  32849  bj-axrep2  32914  bj-nalset  32919  bj-el  32921  bj-dtru  32922  bj-dvdemo1  32927  bj-dvdemo2  32928  ax6er  32945  bj-vtoclf  33033  wl-exeq  33451  spd  42750  elpglem2  42783  eximp-surprise2  42859
  Copyright terms: Public domain W3C validator