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

Theorem exlimiiv 1785
Description: Inference associated with exlimiv 1784. (Contributed by BJ, 19-Dec-2020.)
Hypotheses
Ref Expression
exlimiv.1  |-  ( ph  ->  ps )
exlimiiv.2  |-  E. x ph
Assertion
Ref Expression
exlimiiv  |-  ps
Distinct variable group:    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem exlimiiv
StepHypRef Expression
1 exlimiiv.2 . 2  |-  E. x ph
2 exlimiv.1 . . 3  |-  ( ph  ->  ps )
32exlimiv 1784 . 2  |-  ( E. x ph  ->  ps )
41, 3ax-mp 5 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   E.wex 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766
This theorem depends on definitions:  df-bi 190  df-ex 1672
This theorem is referenced by:  equid  1863  ax7  1868  ax12v2  1952  ax12vOLD  1953  ax12vOLDOLD  1954  19.8a  1955  ax6e  2107  axc11n  2157  axc11nOLD  2158  axc11nALT  2159  axext3  2453  bm1.3ii  4521  inf3  8158  epfrs  8233  kmlem2  8599  axcc2lem  8884  dcomex  8895  axdclem2  8968  grothpw  9269  grothpwex  9270  grothomex  9272  grothac  9273  cnso  14376  aannenlem3  23365  bj-ax6e  31330  bj-axc11nv  31414
  Copyright terms: Public domain W3C validator