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

Theorem eximii 1912
Description: Inference associated with eximi 1910. (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 1910 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
41, 3ax-mp 5 1 𝑥𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885
This theorem depends on definitions:  df-bi 197  df-ex 1853
This theorem is referenced by:  exiftru  2060  spimeh  2083  ax6evr  2100  spimv1  2278  ax6e  2412  spim  2416  spimed  2417  spimvALT  2420  spei  2423  equvini  2492  equvel  2493  euequ1  2624  euex  2642  darii  2714  barbari  2716  festino  2720  baroco  2721  cesaro  2722  camestros  2723  datisi  2724  disamis  2725  felapton  2728  darapti  2729  dimatis  2731  fresison  2732  calemos  2733  fesapo  2734  bamalip  2735  vtoclf  3410  vtocl  3411  axrep2  4908  axnul  4923  nalset  4930  notzfaus  4972  el  4979  dtru  4989  eusv2nf  4996  dvdemo1  5031  dvdemo2  5032  axpr  5034  snnexOLD  7115  inf1  8684  bnd  8920  axpowndlem2  9623  grothomex  9854  bnj101  31130  axextdfeq  32040  ax8dfeq  32041  axextndbi  32047  snelsingles  32367  bj-ax6elem2  32990  bj-spimedv  33057  bj-spimvv  33059  bj-speiv  33062  bj-axrep2  33126  bj-nalset  33131  bj-el  33133  bj-dtru  33134  bj-dvdemo1  33139  bj-dvdemo2  33140  ax6er  33156  bj-vtoclf  33239  wl-exeq  33657  spd  42954  elpglem2  42987  eximp-surprise2  43063
  Copyright terms: Public domain W3C validator