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

Theorem eximii 1534
Description: Inference associated with eximi 1532. (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 1532 . 2  |-  ( E. x ph  ->  E. x ps )
41, 3ax-mp 7 1  |-  E. x ps
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-ial 1468
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  spimed  1669  darii  2042  barbari  2044  festino  2048  baroco  2049  cesaro  2050  camestros  2051  datisi  2052  disamis  2053  felapton  2056  darapti  2057  dimatis  2059  fresison  2060  calemos  2061  fesapo  2062  bamalip  2063  vtoclf  2653  vtocl2  2655  vtocl3  2656  nalset  3916  el  3960  dtruarb  3970  snnex  4207  eusv2nf  4214  dtruex  4310  limom  4362  bj-axemptylem  10841  bj-nalset  10844  bj-d0clsepcl  10878  bj-omex2  10930  bj-nn0sucALT  10931
  Copyright terms: Public domain W3C validator