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

Theorem eximii 1564
Description: Inference associated with eximi 1562. (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 1562 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
41, 3ax-mp 5 1 𝑥𝜓
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1451
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-ial 1497
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ax6evr  1664  spimed  1701  darii  2075  barbari  2077  festino  2081  baroco  2082  cesaro  2083  camestros  2084  datisi  2085  disamis  2086  felapton  2089  darapti  2090  dimatis  2092  fresison  2093  calemos  2094  fesapo  2095  bamalip  2096  vtoclf  2711  vtocl2  2713  vtocl3  2714  nalset  4026  el  4070  dtruarb  4083  snnex  4337  eusv2nf  4345  dtruex  4442  limom  4495  bj-axemptylem  12892  bj-nalset  12895  bj-d0clsepcl  12925  bj-omex2  12977  bj-nn0sucALT  12978
  Copyright terms: Public domain W3C validator