Theorem a1bi 337

Description: Inference rule introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)

Hypothesis

Ref	Expression
a1bi.1

Assertion

Ref	Expression
a1bi

Proof of Theorem a1bi

Step	Hyp	Ref	Expression
1		a1bi.1	. 2
2		biimt 335	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  ->wi 4  <->wb 184

This theorem is referenced by:  mt2bi  338  pm4.83  929  truimfal  1428  equsalhw  1945  equsal  2036  sbequ8ALT  2148  ralv  3123  reusv5OLD  4662  relop  5158  acsfn0  15057  cmpsub  19900  ballotlemodife  28436  wl-equsald  29992  bj-trut  34171  bj-equsalv  34309  bj-equsalvv  34310  bj-ralvw  34441  lub0N  34914  glb0N  34918

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185