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

Theorem eximii 1509
 Description: Inference associated with eximi 1507. (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 1507 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
41, 3ax-mp 7 1 𝑥𝜓
 Colors of variables: wff set class Syntax hints:   → wi 4  ∃wex 1397 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-ial 1443 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  spimed  1644  darii  2016  barbari  2018  festino  2022  baroco  2023  cesaro  2024  camestros  2025  datisi  2026  disamis  2027  felapton  2030  darapti  2031  dimatis  2033  fresison  2034  calemos  2035  fesapo  2036  bamalip  2037  vtoclf  2624  vtocl2  2626  vtocl3  2627  nalset  3915  el  3959  dtruarb  3970  snnex  4209  eusv2nf  4216  limom  4364  bj-axemptylem  10399  bj-nalset  10402  bj-d0clsepcl  10436  bj-omex2  10489  bj-nn0sucALT  10490
 Copyright terms: Public domain W3C validator