Theorem iba 526

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 470	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))
2		simpl 481	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜓)
3	1, 2	impbid1 224	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  ibar  527  biantru  528  biantrud  530  ancrb  546  pm5.54  1015  dedlem0a  1041  r19.29r  3109  unineq  4289  fvopab6  7048  fressnfv  7179  tpostpos  8269  odi  8617  nnmword  8671  ltmpi  10954  maducoeval2  22656  mdbr2  32252  mdsl2i  32278  poimirlem26  37394  poimirlem27  37395  itg2addnclem  37419  itg2addnclem3  37421  prjspeclsp  42336  rmydioph  42743  expdioph  42752  dmafv2rnb  46912