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

Theorem exlimiiv 1934
Description: Inference (Rule C) associated with exlimiv 1933. (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 1933 . 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 1913
This theorem depends on definitions:  df-bi 206  df-ex 1782
This theorem is referenced by:  equid  2015  ax7  2019  sbcom2  2161  ax12v2  2173  19.8a  2174  ax6e  2381  axc11n  2424  vtocl  3546  bm1.3ii  5295  axprlem1  5414  axprlem2  5415  axpr  5419  inf3  9612  epfrs  9708  kmlem2  10128  axcc2lem  10413  dcomex  10424  axdclem2  10497  grothpw  10803  grothpwex  10804  grothomex  10806  grothac  10807  cnso  16172  aannenlem3  25772  bj-ax12  35336  bj-ax6e  35347  wl-spae  36192
  Copyright terms: Public domain W3C validator