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 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911
This theorem depends on definitions:  df-bi 206  df-ex 1780
This theorem is referenced by:  equid  2013  ax7  2017  sbcom2  2159  ax12v2  2171  19.8a  2172  ax6e  2380  axc11n  2423  vtocl  3544  bm1.3ii  5301  axprlem1  5420  axprlem2  5421  axpr  5425  inf3  9632  epfrs  9728  kmlem2  10148  axcc2lem  10433  dcomex  10444  axdclem2  10517  grothpw  10823  grothpwex  10824  grothomex  10826  grothac  10827  cnso  16194  aannenlem3  26079  bj-ax12  35837  bj-ax6e  35848  wl-spae  36693
  Copyright terms: Public domain W3C validator