Theorem a2i 13

Description: Inference derived from axiom ax-2 7. (Contributed by NM, 29-Dec-1992.)

Hypothesis

Ref	Expression
a2i.1

Assertion

Ref	Expression
a2i

Proof of Theorem a2i

Step	Hyp	Ref	Expression
1		a2i.1	. 2
2		ax-2 7	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  ->wi 4

This theorem is referenced by:  imim2i  14  mpd  15  sylcom  29  pm2.43  51  pm2.18  110  ancl  546  ancr  549  anc2r  556  hbim1  1918  ralimia  2848  ceqsalgALT  3135  rspct  3203  elabgt  3243  fvmptt  5971  tfi  6688  fnfi  7818  finsschain  7847  ordiso2  7961  ordtypelem7  7970  dfom3  8085  infdiffi  8095  cantnfp1lem3  8120  cantnf  8133  cantnfp1lem3OLD  8146  cantnfOLD  8155  r1ordg  8217  ttukeylem6  8915  fpwwe2lem8  9036  wunfi  9120  dfnn2  10574  psgnunilem3  16521  pgpfac1  17131  fiuncmp  19904  filssufilg  20412  ufileu  20420  pjnormssi  27087  waj-ax  29879  wl-mps  29971  atbiffatnnb  32108  bnj1110  34038  bj-equsal1  34397  bj-equsal2  34398

This theorem was proved from axioms:  ax-mp 5  ax-2 7