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

Theorem exlimiiv 1926
Description: Inference (Rule C) associated with exlimiv 1925. (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 1925 . 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  ax-5 1905
This theorem depends on definitions:  df-bi 206  df-ex 1774
This theorem is referenced by:  equid  2007  ax7  2011  sbcom2  2153  ax12v2  2165  19.8a  2166  ax6e  2376  axc11n  2419  vtocl  3540  bm1.3ii  5295  axprlem1  5414  axprlem2  5415  axpr  5419  inf3  9632  epfrs  9728  kmlem2  10148  axcc2lem  10433  dcomex  10444  axdclem2  10517  grothpw  10823  grothpwex  10824  grothomex  10826  grothac  10827  cnso  16197  aannenlem3  26220  bj-ax12  36042  bj-ax6e  36053  wl-spae  36897
  Copyright terms: Public domain W3C validator