Theorem iba 529

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 473	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))
2		simpl 484	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜓)
3	1, 2	impbid1 224	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  ibar  530  biantru  531  biantrud  533  ancrb  549  pm5.54  1017  dedlem0a  1043  r19.29r  3117  unineq  4278  fvopab6  7032  fressnfv  7158  tpostpos  8231  odi  8579  nnmword  8633  ltmpi  10899  maducoeval2  22142  mdbr2  31549  mdsl2i  31575  poimirlem26  36514  poimirlem27  36515  itg2addnclem  36539  itg2addnclem3  36541  prjspeclsp  41354  rmydioph  41753  expdioph  41762  dmafv2rnb  45937