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

Theorem eximii 1536
Description: Inference associated with eximi 1534. (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 1534 . 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 1424
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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-ial 1470
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  ax6evr  1636  spimed  1672  darii  2045  barbari  2047  festino  2051  baroco  2052  cesaro  2053  camestros  2054  datisi  2055  disamis  2056  felapton  2059  darapti  2060  dimatis  2062  fresison  2063  calemos  2064  fesapo  2065  bamalip  2066  vtoclf  2666  vtocl2  2668  vtocl3  2669  nalset  3943  el  3987  dtruarb  3999  snnex  4244  eusv2nf  4251  dtruex  4347  limom  4400  bj-axemptylem  11213  bj-nalset  11216  bj-d0clsepcl  11250  bj-omex2  11302  bj-nn0sucALT  11303
  Copyright terms: Public domain W3C validator