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  1018  dedlem0a  1044  r19.29r  3122  unineq  4307  fvopab6  7063  fressnfv  7194  tpostpos  8287  odi  8635  nnmword  8689  ltmpi  10973  maducoeval2  22667  mdbr2  32328  mdsl2i  32354  poimirlem26  37606  poimirlem27  37607  itg2addnclem  37631  itg2addnclem3  37633  prjspeclsp  42567  rmydioph  42971  expdioph  42980  dmafv2rnb  47144