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  4229  fvopab6  6978  fressnfv  7109  tpostpos  8191  odi  8509  nnmword  8564  ltmpi  10822  maducoeval2  22619  mdbr2  32386  mdsl2i  32412  poimirlem26  37987  poimirlem27  37988  itg2addnclem  38012  itg2addnclem3  38014  xpv  38603  prjspeclsp  43065  rmydioph  43466  expdioph  43475  dmafv2rnb  47695