Theorem iba 524

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  biantru  526  biantrud  528  ancrb  573  pm5.54  943  rbaibr  946  rbaibd  949  dedlem0a  1000  unineq  3877  fvopab6  6310  fressnfv  6427  tpostpos  7372  odi  7659  nnmword  7713  ltmpi  9726  maducoeval2  20446  hausdiag  21448  mdbr2  29155  mdsl2i  29181  poimirlem26  33435  poimirlem27  33436  itg2addnclem  33461  itg2addnclem3  33463  rmydioph  37581  expdioph  37590