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

Theorem eximii 1602
Description: Inference associated with eximi 1600. (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 1600 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
41, 3ax-mp 5 1 𝑥𝜓
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  spimfv  1699  ax6evr  1705  spimed  1740  darii  2126  barbari  2128  festino  2132  baroco  2133  cesaro  2134  camestros  2135  datisi  2136  disamis  2137  felapton  2140  darapti  2141  dimatis  2143  fresison  2144  calemos  2145  fesapo  2146  bamalip  2147  vtoclf  2790  vtocl2  2792  vtocl3  2793  nalset  4132  el  4177  dtruarb  4190  snnex  4447  eusv2nf  4455  dtruex  4557  limom  4612  bj-axemptylem  14504  bj-nalset  14507  bj-d0clsepcl  14537  bj-omex2  14589  bj-nn0sucALT  14590
  Copyright terms: Public domain W3C validator