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 224	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397

This theorem is referenced by:  ibar  529  biantru  530  biantrud  532  ancrb  548  pm5.54  1015  dedlem0a  1041  unineq  4211  fvopab6  6908  fressnfv  7032  tpostpos  8062  odi  8410  nnmword  8464  ltmpi  10660  maducoeval2  21789  mdbr2  30658  mdsl2i  30684  poimirlem26  35803  poimirlem27  35804  itg2addnclem  35828  itg2addnclem3  35830  prjspeclsp  40451  rmydioph  40836  expdioph  40845  dmafv2rnb  44721