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  4228  fvopab6  6982  fressnfv  7114  tpostpos  8196  odi  8514  nnmword  8569  ltmpi  10827  maducoeval2  22605  mdbr2  32367  mdsl2i  32393  poimirlem26  37967  poimirlem27  37968  itg2addnclem  37992  itg2addnclem3  37994  xpv  38583  prjspeclsp  43045  rmydioph  43442  expdioph  43451  dmafv2rnb  47677