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

Theorem eximii 1742
Description: Inference associated with eximi 1740. (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 1740 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
41, 3ax-mp 5 1 𝑥𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  exiftru  1841  spimeh  1875  ax6evr  1892  spimv1  2109  cbv3hvOLD  2113  cbv3hvOLDOLD  2114  ax6e  2141  spim  2145  spimed  2146  spimv  2148  spei  2152  equvini  2238  equvel  2239  euequ1  2368  euex  2386  darii  2457  barbari  2459  festino  2463  baroco  2464  cesaro  2465  camestros  2466  datisi  2467  disamis  2468  felapton  2471  darapti  2472  dimatis  2474  fresison  2475  calemos  2476  fesapo  2477  bamalip  2478  vtoclf  3135  vtocl  3136  axrep2  4599  axnul  4614  nalset  4622  notzfaus  4665  el  4672  dtru  4682  eusv2nf  4689  dvdemo1  4728  dvdemo2  4729  axpr  4731  snnex  6737  inf1  8277  bnd  8513  axpowndlem2  9174  grothomex  9405  bnj101  29889  axextdfeq  30790  ax8dfeq  30791  axextndbi  30797  snelsingles  31035  bj-ax6elem2  31676  bj-spimedv  31741  bj-spimvv  31743  bj-speiv  31746  bj-axrep2  31819  bj-nalset  31824  bj-el  31826  bj-dtru  31827  bj-dvdemo1  31832  bj-dvdemo2  31833  ax6er  31850  bj-vtoclf  31932  wl-exeq  32374  eximp-surprise2  42393
  Copyright terms: Public domain W3C validator