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  1019  dedlem0a  1043  r19.29r  3115  unineq  4287  fvopab6  7049  fressnfv  7179  tpostpos  8272  odi  8618  nnmword  8672  ltmpi  10945  maducoeval2  22647  mdbr2  32316  mdsl2i  32342  poimirlem26  37654  poimirlem27  37655  itg2addnclem  37679  itg2addnclem3  37681  prjspeclsp  42627  rmydioph  43031  expdioph  43040  dmafv2rnb  47246