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

Theorem eximii 1493
Description: Inference associated with eximi 1491. (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 1491 . 2 (∃𝑥𝜑 → ∃𝑥𝜓)
41, 3ax-mp 7 1 𝑥𝜓
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1381
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-ial 1427
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  spimed  1628  darii  2000  barbari  2002  festino  2006  baroco  2007  cesaro  2008  camestros  2009  datisi  2010  disamis  2011  felapton  2014  darapti  2015  dimatis  2017  fresison  2018  calemos  2019  fesapo  2020  bamalip  2021  vtoclf  2607  vtocl2  2609  vtocl3  2610  nalset  3887  el  3931  dtruarb  3942  snnex  4181  eusv2nf  4188  limom  4336  bj-axemptylem  10012  bj-nalset  10015  bj-d0clsepcl  10049  bj-omex2  10102  bj-nn0sucALT  10103
  Copyright terms: Public domain W3C validator