Theorem iba 523

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 463	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))
2		simpl 472	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜓)
3	1, 2	impbid1 214	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  biantru  525  biantrud  527  ancrb  571  pm5.54  941  rbaibr  944  rbaibd  947  dedlem0a  991  unineq  3836  fvopab6  6218  fressnfv  6332  tpostpos  7259  odi  7546  nnmword  7600  ltmpi  9605  maducoeval2  20265  hausdiag  21258  mdbr2  28539  mdsl2i  28565  poimirlem26  32605  poimirlem27  32606  itg2addnclem  32631  itg2addnclem3  32633  rmydioph  36599  expdioph  36608