MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eximii Unicode version

Theorem eximii 1658
Description: Inference associated with eximi 1656. (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 1656 . 2
41, 3ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E.wex 1612
This theorem is referenced by:  exiftru  1750  spimeh  1782  equid  1791  cbv3hv  1956  ax6e  2002  spim  2006  spimed  2007  spei  2012  equvini  2087  equveli  2088  equveliOLD  2089  euequ1  2288  euex  2308  darii  2398  barbari  2400  festino  2404  baroco  2405  cesaro  2406  camestros  2407  datisi  2408  disamis  2409  felapton  2412  darapti  2413  dimatis  2415  fresison  2416  calemos  2417  fesapo  2418  bamalip  2419  vtoclf  3160  axrep2  4565  nalset  4589  notzfaus  4627  el  4634  dtru  4643  eusv2nf  4650  dvdemo1  4687  dvdemo2  4688  axpr  4690  snnex  6606  inf1  8060  bnd  8331  axpowndlem2  8994  grothomex  9228  axextdfeq  29230  ax8dfeq  29231  axextndbi  29237  snelsingles  29572  wl-exeq  29987  eximp-surprise2  33200  bnj101  33776  bj-spimv  34279  bj-spimedv  34280  bj-speiv  34285  bj-axrep2  34375  bj-nalset  34380  bj-el  34382  bj-dtru  34383  bj-dvdemo1  34388  bj-dvdemo2  34389  ax6er  34406  bj-vtoclf  34480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator