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

Theorem exlimiiv 1932
Description: Inference (Rule C) associated with exlimiv 1931. (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 1931 . 2 (∃𝑥𝜑𝜓)
41, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem depends on definitions:  df-bi 210  df-ex 1782
This theorem is referenced by:  equid  2019  ax7  2023  sbcom2  2168  ax12v2  2180  19.8a  2181  ax6e  2402  axc11n  2449  vtocl  3534  bm1.3ii  5182  axprlem1  5301  axprlem2  5302  axpr  5306  inf3  9086  epfrs  9161  kmlem2  9566  axcc2lem  9847  dcomex  9858  axdclem2  9931  grothpw  10237  grothpwex  10238  grothomex  10240  grothac  10241  cnso  15591  aannenlem3  24924  bj-ax12  34064  bj-ax6e  34075  wl-spae  34884
  Copyright terms: Public domain W3C validator