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

Theorem axc4i 1898
 Description: Inference version of axc4 1860. (Contributed by NM, 3-Jan-1993.)
Hypothesis
Ref Expression
axc4i.1
Assertion
Ref Expression
axc4i

Proof of Theorem axc4i
StepHypRef Expression
1 nfa1 1897 . 2
2 axc4i.1 . 2
31, 2alrimi 1877 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  A.wal 1393 This theorem is referenced by:  hbae  2055  hbsb2  2099  hbsb2a  2101  hbsb2e  2102  reu6  3288  axunndlem1  8991  axregndOLD  9003  axacndlem3  9008  axacndlem5  9010  axacnd  9011  pm11.57  31295  pm11.59  31297  axc5c4c711toc7  31311  axc11next  31313  hbalg  33328  ax6e2eq  33330  ax6e2eqVD  33707  bj-nfs1t  34274  bj-hbsb2v  34339  bj-hbsb2av  34341  bj-hbaeb2  34391 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854 This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617
 Copyright terms: Public domain W3C validator