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

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

This theorem is referenced by:  ibar  528  biantru  529  biantrud  531  ancrb  547  pm5.54  1014  dedlem0a  1040  unineq  4208  fvopab6  6890  fressnfv  7014  tpostpos  8033  odi  8372  nnmword  8426  ltmpi  10591  maducoeval2  21697  mdbr2  30559  mdsl2i  30585  poimirlem26  35730  poimirlem27  35731  itg2addnclem  35755  itg2addnclem3  35757  prjspeclsp  40372  rmydioph  40752  expdioph  40761  dmafv2rnb  44608