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  4744  inf3  8476  epfrs  8551  kmlem2  8917  axcc2lem  9202  dcomex  9213  axdclem2  9286  grothpw  9592  grothpwex  9593  grothomex  9595  grothac  9596  cnso  14901  aannenlem3  23989  bj-ax6e  32292  wl-spae  32935
  Copyright terms: Public domain W3C validator