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  572  pm5.54  942  rbaibr  945  rbaibd  948  dedlem0a  999  unineq  3858  fvopab6  6267  fressnfv  6382  tpostpos  7318  odi  7605  nnmword  7659  ltmpi  9671  maducoeval2  20360  hausdiag  21353  mdbr2  28995  mdsl2i  29021  poimirlem26  33053  poimirlem27  33054  itg2addnclem  33079  itg2addnclem3  33081  rmydioph  37047  expdioph  37056