Theorem iba 526

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

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

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 395

This theorem is referenced by:  ibar  527  biantru  528  biantrud  530  ancrb  546  pm5.54  1014  dedlem0a  1040  r19.29r  3114  unineq  4278  fvopab6  7032  fressnfv  7161  tpostpos  8235  odi  8583  nnmword  8637  ltmpi  10903  maducoeval2  22364  mdbr2  31814  mdsl2i  31840  poimirlem26  36819  poimirlem27  36820  itg2addnclem  36844  itg2addnclem3  36846  prjspeclsp  41658  rmydioph  42057  expdioph  42066  dmafv2rnb  46237