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

Theorem eximii 1490
Description: Inference associated with eximi 1488. (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 1488 . 2
41, 3ax-mp 7 1
Colors of variables: wff set class
Syntax hints:   wi 4  wex 1378
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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-ial 1424
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  spimed  1625  darii  1997  barbari  1999  festino  2003  baroco  2004  cesaro  2005  camestros  2006  datisi  2007  disamis  2008  felapton  2011  darapti  2012  dimatis  2014  fresison  2015  calemos  2016  fesapo  2017  bamalip  2018  vtoclf  2601  vtocl2  2603  vtocl3  2604  nalset  3878  el  3922  dtruarb  3933  snnex  4147  eusv2nf  4154  limom  4279  bj-axempty  9347  bj-nalset  9348  bj-d0clsepcl  9382  bj-omex2  9431  bj-nn0sucALT  9432
  Copyright terms: Public domain W3C validator