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

Theorem eximii 1581
Description: Inference associated with eximi 1579. (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 1579 . 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 1468
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ax6evr  1681  spimed  1718  darii  2099  barbari  2101  festino  2105  baroco  2106  cesaro  2107  camestros  2108  datisi  2109  disamis  2110  felapton  2113  darapti  2114  dimatis  2116  fresison  2117  calemos  2118  fesapo  2119  bamalip  2120  vtoclf  2739  vtocl2  2741  vtocl3  2742  nalset  4058  el  4102  dtruarb  4115  snnex  4369  eusv2nf  4377  dtruex  4474  limom  4527  bj-axemptylem  13143  bj-nalset  13146  bj-d0clsepcl  13176  bj-omex2  13228  bj-nn0sucALT  13229
  Copyright terms: Public domain W3C validator