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

Theorem eximii 1582
 Description: Inference associated with eximi 1580. (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 1580 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
41, 3ax-mp 5 1 𝑥𝜓
 Colors of variables: wff set class Syntax hints:   → wi 4  ∃wex 1472 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 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-ial 1514 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  spimfv  1679  ax6evr  1685  spimed  1720  darii  2106  barbari  2108  festino  2112  baroco  2113  cesaro  2114  camestros  2115  datisi  2116  disamis  2117  felapton  2120  darapti  2121  dimatis  2123  fresison  2124  calemos  2125  fesapo  2126  bamalip  2127  vtoclf  2765  vtocl2  2767  vtocl3  2768  nalset  4094  el  4138  dtruarb  4151  snnex  4406  eusv2nf  4414  dtruex  4516  limom  4571  bj-axemptylem  13426  bj-nalset  13429  bj-d0clsepcl  13459  bj-omex2  13511  bj-nn0sucALT  13512
 Copyright terms: Public domain W3C validator