Theorem iba 530

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 474	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))
2		simpl 485	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜓)
3	1, 2	impbid1 227	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  ibar  531  biantru  532  biantrud  534  ancrb  550  pm5.54  1014  dedlem0a  1038  unineq  4256  fvopab6  6803  fressnfv  6924  tpostpos  7914  odi  8207  nnmword  8261  ltmpi  10328  maducoeval2  21251  mdbr2  30075  mdsl2i  30101  poimirlem26  34920  poimirlem27  34921  itg2addnclem  34945  itg2addnclem3  34947  prjspeclsp  39269  rmydioph  39618  expdioph  39627  dmafv2rnb  43435