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

Theorem eximii 1740
Description: Inference associated with eximi 1738. (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 1738 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
41, 3ax-mp 5 1 𝑥𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711
This theorem depends on definitions:  df-bi 192  df-ex 1693
This theorem is referenced by:  exiftru  1839  spimeh  1873  equidOLD  1888  ax6evr  1891  spimv1  2110  cbv3hvOLD  2114  cbv3hvOLDOLD  2115  ax6e  2141  spim  2145  spimed  2146  spimv  2148  spei  2152  equvini  2229  equvel  2230  euequ1  2359  euex  2377  darii  2448  barbari  2450  festino  2454  baroco  2455  cesaro  2456  camestros  2457  datisi  2458  disamis  2459  felapton  2462  darapti  2463  dimatis  2465  fresison  2466  calemos  2467  fesapo  2468  bamalip  2469  vtoclf  3120  vtocl  3121  axrep2  4550  axnul  4565  nalset  4573  notzfaus  4616  el  4623  dtru  4633  eusv2nf  4640  dvdemo1  4676  dvdemo2  4677  axpr  4679  snnex  6674  inf1  8212  bnd  8448  axpowndlem2  9108  grothomex  9339  bnj101  29682  axextdfeq  30595  ax8dfeq  30596  axextndbi  30602  snelsingles  30840  bj-ax6elem2  31447  bj-spimedv  31507  bj-spimvv  31509  bj-speiv  31512  bj-axrep2  31586  bj-nalset  31591  bj-el  31593  bj-dtru  31594  bj-dvdemo1  31599  bj-dvdemo2  31600  ax6er  31617  bj-vtoclf  31699  wl-exeq  32098  eximp-surprise2  41711
  Copyright terms: Public domain W3C validator