Theorem iba 528

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ibar  529  biantru  530  biantrud  532  ancrb  548  pm5.54  1012  dedlem0a  1036  unineq  4180  fvopab6  6673  fressnfv  6792  tpostpos  7770  odi  8062  nnmword  8116  ltmpi  10179  maducoeval2  20937  mdbr2  29760  mdsl2i  29786  poimirlem26  34470  poimirlem27  34471  itg2addnclem  34495  itg2addnclem3  34497  prjspeclsp  38780  rmydioph  39117  expdioph  39126  dmafv2rnb  42966