Theorem iba 527

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 471	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))
2		simpl 482	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜓)
3	1, 2	impbid1 225	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ibar  528  biantru  529  biantrud  531  ancrb  547  pm5.54  1020  dedlem0a  1044  r19.29r  3102  unineq  4242  fvopab6  6986  fressnfv  7117  tpostpos  8200  odi  8518  nnmword  8573  ltmpi  10829  maducoeval2  22601  mdbr2  32390  mdsl2i  32416  poimirlem26  37926  poimirlem27  37927  itg2addnclem  37951  itg2addnclem3  37953  xpv  38542  prjspeclsp  42999  rmydioph  43400  expdioph  43409  dmafv2rnb  47618