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

Theorem eximii 1753
Description: Inference associated with eximi 1751. (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 1751 . 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 1712  ax-4 1727
This theorem depends on definitions:  df-bi 195  df-ex 1695
This theorem is referenced by:  exiftru  1877  spimeh  1911  ax6evr  1928  spimv1  2099  cbv3hvOLD  2159  cbv3hvOLDOLD  2160  ax6e  2236  spim  2240  spimed  2241  spimv  2243  spei  2247  equvini  2333  equvel  2334  euequ1  2463  euex  2481  darii  2552  barbari  2554  festino  2558  baroco  2559  cesaro  2560  camestros  2561  datisi  2562  disamis  2563  felapton  2566  darapti  2567  dimatis  2569  fresison  2570  calemos  2571  fesapo  2572  bamalip  2573  vtoclf  3230  vtocl  3231  axrep2  4695  axnul  4710  nalset  4718  notzfaus  4761  el  4768  dtru  4778  eusv2nf  4785  dvdemo1  4824  dvdemo2  4825  axpr  4827  snnex  6839  inf1  8379  bnd  8615  axpowndlem2  9276  grothomex  9507  bnj101  29849  axextdfeq  30753  ax8dfeq  30754  axextndbi  30760  snelsingles  31005  bj-ax6elem2  31647  bj-spimedv  31712  bj-spimvv  31714  bj-speiv  31717  bj-axrep2  31790  bj-nalset  31795  bj-el  31797  bj-dtru  31798  bj-dvdemo1  31803  bj-dvdemo2  31804  ax6er  31821  bj-vtoclf  31903  wl-exeq  32303  eximp-surprise2  42303
  Copyright terms: Public domain W3C validator