ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eximii Unicode version

Theorem eximii 1595
Description: Inference associated with eximi 1593. (Contributed by BJ, 3-Feb-2018.)
Hypotheses
Ref Expression
eximii.1  |-  E. x ph
eximii.2  |-  ( ph  ->  ps )
Assertion
Ref Expression
eximii  |-  E. x ps

Proof of Theorem eximii
StepHypRef Expression
1 eximii.1 . 2  |-  E. x ph
2 eximii.2 . . 3  |-  ( ph  ->  ps )
32eximi 1593 . 2  |-  ( E. x ph  ->  E. x ps )
41, 3ax-mp 5 1  |-  E. x ps
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1485
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-ial 1527
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  spimfv  1692  ax6evr  1698  spimed  1733  darii  2119  barbari  2121  festino  2125  baroco  2126  cesaro  2127  camestros  2128  datisi  2129  disamis  2130  felapton  2133  darapti  2134  dimatis  2136  fresison  2137  calemos  2138  fesapo  2139  bamalip  2140  vtoclf  2783  vtocl2  2785  vtocl3  2786  nalset  4117  el  4162  dtruarb  4175  snnex  4431  eusv2nf  4439  dtruex  4541  limom  4596  bj-axemptylem  13892  bj-nalset  13895  bj-d0clsepcl  13925  bj-omex2  13977  bj-nn0sucALT  13978
  Copyright terms: Public domain W3C validator