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

Theorem exlimiiv 1996
Description: Inference associated with exlimiv 1995. (Contributed by BJ, 19-Dec-2020.)
Hypotheses
Ref Expression
exlimiv.1 (𝜑𝜓)
exlimiiv.2 𝑥𝜑
Assertion
Ref Expression
exlimiiv 𝜓
Distinct variable group:   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem exlimiiv
StepHypRef Expression
1 exlimiiv.2 . 2 𝑥𝜑
2 exlimiv.1 . . 3 (𝜑𝜓)
32exlimiv 1995 . 2 (∃𝑥𝜑𝜓)
41, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976
This theorem depends on definitions:  df-bi 197  df-ex 1842
This theorem is referenced by:  equid  2082  ax7  2086  ax12v2  2186  19.8a  2187  ax6e  2383  axc11n  2439  axc11nOLD  2440  axext3  2730  bm1.3ii  4924  inf3  8693  epfrs  8768  kmlem2  9136  axcc2lem  9421  dcomex  9432  axdclem2  9505  grothpw  9811  grothpwex  9812  grothomex  9814  grothac  9815  cnso  15146  aannenlem3  24255  bj-ax6e  32930  wl-spae  33588
  Copyright terms: Public domain W3C validator