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

Theorem exlimiiv 1923
Description: Inference (Rule C) associated with exlimiv 1922. (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 1922 . 2 (∃𝑥𝜑𝜓)
41, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-ex 1772
This theorem is referenced by:  equid  2010  ax7  2014  sbcom2  2158  ax12v2  2169  19.8a  2170  ax6e  2392  axc11n  2440  bm1.3ii  5197  axprlem1  5314  axprlem2  5315  axpr  5319  inf3  9086  epfrs  9161  kmlem2  9565  axcc2lem  9846  dcomex  9857  axdclem2  9930  grothpw  10236  grothpwex  10237  grothomex  10239  grothac  10240  cnso  15588  aannenlem3  24846  bj-ax12  33887  bj-ax6e  33898  wl-spae  34643
  Copyright terms: Public domain W3C validator