Theorem iba 503

Description: Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.)

Assertion

Ref	Expression
iba

Proof of Theorem iba

Step	Hyp	Ref	Expression
1		pm3.21 448	. 2
2		simpl 457	. 2
3	1, 2	impbid1 203	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369

This theorem is referenced by:  biantru  505  biantrud  507  ancrb  550  pm5.54  902  rbaibr  905  rbaibd  910  dedlem0a  952  unineq  3747  fvopab6  5980  fressnfv  6085  tpostpos  6994  odi  7247  nnmword  7301  ltmpi  9303  maducoeval2  19142  hausdiag  20146  numclwwlkun  25079  mdbr2  27215  mdsl2i  27241  itg2addnclem  30066  itg2addnclem3  30068  rmydioph  30956  expdioph  30965

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  df-an 371