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

Theorem eximii 1830
 Description: Inference associated with eximi 1828. (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 1828 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
41, 3ax-mp 5 1 𝑥𝜓
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wex 1773 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803 This theorem depends on definitions:  df-bi 208  df-ex 1774 This theorem is referenced by:  exan  1855  exanOLD  1856  spimehOLD  1968  exgenOLD  1972  ax6evr  2015  spimedv  2190  spimfv  2234  ax6e  2396  spim  2401  spimed  2402  spimvALT  2405  spei  2408  equvini  2474  equviniOLD  2475  equvel  2476  equsb1vOLDOLD  2515  euequ  2680  euequOLD  2681  dariiALT  2753  barbariALT  2757  festinoALT  2762  barocoALT  2764  daraptiALT  2772  vtoclf  3563  vtocl  3564  axrep2  5189  axnul  5205  nalset  5213  notzfaus  5258  notzfausOLD  5259  el  5266  dtru  5267  dvdemo1  5270  dvdemo2  5271  eusv2nf  5291  axprALT  5318  axpr  5324  inf1  9077  bnd  9313  axpowndlem2  10012  grothomex  10243  tgjustc1  26177  tgjustc2  26178  bnj101  31881  axextdfeq  32928  ax8dfeq  32929  axextndbi  32935  snelsingles  33269  bj-ax6elem2  33886  bj-dtru  34025  ax6er  34042  bj-vtoclf  34117  wl-exeq  34644  sn-el  38977  spd  44615  elpglem2  44648  eximp-surprise2  44720
 Copyright terms: Public domain W3C validator