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

Theorem exlimiiv 1974
Description: Inference (Rule C) associated with exlimiv 1973. (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 1973 . 2 (∃𝑥𝜑𝜓)
41, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953
This theorem depends on definitions:  df-bi 199  df-ex 1824
This theorem is referenced by:  equid  2059  ax7  2063  ax12v2  2165  19.8a  2166  ax6e  2347  axc11n  2392  sbcom2  2523  axext3  2756  bm1.3ii  5022  inf3  8831  epfrs  8906  kmlem2  9310  axcc2lem  9595  dcomex  9606  axdclem2  9679  grothpw  9985  grothpwex  9986  grothomex  9988  grothac  9989  cnso  15384  aannenlem3  24526  bj-ax6e  33247  wl-spae  33905
  Copyright terms: Public domain W3C validator