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

Theorem eximii 1590
Description: Inference associated with eximi 1588. (Contributed by BJ, 3-Feb-2018.)
Hypotheses
Ref Expression
eximii.1 𝑥𝜑
eximii.2 (𝜑𝜓)
Assertion
Ref Expression
eximii 𝑥𝜓

Proof of Theorem eximii
StepHypRef Expression
1 eximii.1 . 2 𝑥𝜑
2 eximii.2 . . 3 (𝜑𝜓)
32eximi 1588 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
41, 3ax-mp 5 1 𝑥𝜓
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1480
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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-ial 1522
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  spimfv  1687  ax6evr  1693  spimed  1728  darii  2114  barbari  2116  festino  2120  baroco  2121  cesaro  2122  camestros  2123  datisi  2124  disamis  2125  felapton  2128  darapti  2129  dimatis  2131  fresison  2132  calemos  2133  fesapo  2134  bamalip  2135  vtoclf  2779  vtocl2  2781  vtocl3  2782  nalset  4112  el  4157  dtruarb  4170  snnex  4426  eusv2nf  4434  dtruex  4536  limom  4591  bj-axemptylem  13774  bj-nalset  13777  bj-d0clsepcl  13807  bj-omex2  13859  bj-nn0sucALT  13860
  Copyright terms: Public domain W3C validator