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

Theorem eximii 1843
Description: Inference associated with eximi 1841. (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 1841 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
41, 3ax-mp 5 1 𝑥𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816
This theorem depends on definitions:  df-bi 210  df-ex 1787
This theorem is referenced by:  exan  1868  spimehOLD  1979  exgenOLD  1983  ax6evr  2026  spimedv  2198  spimfv  2240  ax6e  2382  spim  2386  spimed  2387  spimvALT  2390  spei  2393  equvini  2454  equvel  2455  euequ  2598  dariiALT  2668  barbariALT  2672  festinoALT  2677  barocoALT  2679  daraptiALT  2687  vtoclf  3462  axrep2  5154  axnul  5170  nalset  5178  notzfaus  5225  notzfausOLD  5226  el  5233  dtru  5234  dvdemo1  5237  dvdemo2  5238  eusv2nf  5259  axprALT  5286  axpr  5292  inf1  9151  bnd  9387  axpowndlem2  10091  grothomex  10322  tgjustc1  26413  tgjustc2  26414  bnj101  32264  axextdfeq  33337  ax8dfeq  33338  axextndbi  33344  snelsingles  33854  bj-ax6elem2  34475  bj-dtru  34619  ax6er  34636  bj-vtoclf  34721  wl-exeq  35305  sn-el  39762  spd  45821  elpglem2  45854  eximp-surprise2  45926
  Copyright terms: Public domain W3C validator