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

Theorem exlimiiv 1856
Description: Inference associated with exlimiv 1855. (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 1855 . 2 (∃𝑥𝜑𝜓)
41, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  equid  1936  ax7  1940  ax12v2  2046  ax12vOLD  2047  ax12vOLDOLD  2048  19.8a  2049  ax6e  2249  axc11n  2306  axc11nOLD  2307  axc11nOLDOLD  2308  axc11nALT  2309  axext3  2603  bm1.3ii  4754  inf3  8492  epfrs  8567  kmlem2  8933  axcc2lem  9218  dcomex  9229  axdclem2  9302  grothpw  9608  grothpwex  9609  grothomex  9611  grothac  9612  cnso  14920  aannenlem3  24023  bj-ax6e  32348  wl-spae  32977
  Copyright terms: Public domain W3C validator