Theorem iba 527

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 471	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))
2		simpl 482	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜓)
3	1, 2	impbid1 225	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ibar  528  biantru  529  biantrud  531  ancrb  547  pm5.54  1020  dedlem0a  1044  r19.29r  3101  unineq  4241  fvopab6  6977  fressnfv  7107  tpostpos  8190  odi  8508  nnmword  8563  ltmpi  10819  maducoeval2  22588  mdbr2  32375  mdsl2i  32401  poimirlem26  37849  poimirlem27  37850  itg2addnclem  37874  itg2addnclem3  37876  xpv  38465  prjspeclsp  42922  rmydioph  43323  expdioph  43332  dmafv2rnb  47542