Theorem iba 529

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

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

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 398

This theorem is referenced by:  ibar  530  biantru  531  biantrud  533  ancrb  549  pm5.54  1017  dedlem0a  1043  r19.29r  3117  unineq  4276  fvopab6  7027  fressnfv  7153  tpostpos  8226  odi  8575  nnmword  8629  ltmpi  10895  maducoeval2  22124  mdbr2  31527  mdsl2i  31553  poimirlem26  36452  poimirlem27  36453  itg2addnclem  36477  itg2addnclem3  36479  prjspeclsp  41298  rmydioph  41686  expdioph  41695  dmafv2rnb  45872