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

Theorem exlimiiv 2011
Description: Inference associated with exlimiv 2010. (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 2010 . 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  ax-5 1991
This theorem depends on definitions:  df-bi 197  df-ex 1853
This theorem is referenced by:  equid  2097  ax7  2101  ax12v2  2205  19.8a  2206  ax6e  2412  axc11n  2462  axext3  2753  bm1.3ii  4918  inf3  8696  epfrs  8771  kmlem2  9175  axcc2lem  9460  dcomex  9471  axdclem2  9544  grothpw  9850  grothpwex  9851  grothomex  9853  grothac  9854  cnso  15182  aannenlem3  24305  bj-ax6e  32990  wl-spae  33643
  Copyright terms: Public domain W3C validator