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

Step	Hyp	Ref	Expression
1		nfa1 1897	. 2
2		axc4i.1	. 2
3	1, 2	alrimi 1877	1

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