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  4254  fvopab6  6796  fressnfv  6917  tpostpos  7906  odi  8199  nnmword  8253  ltmpi  10320  maducoeval2  21243  mdbr2  30067  mdsl2i  30093  poimirlem26  34912  poimirlem27  34913  itg2addnclem  34937  itg2addnclem3  34939  prjspeclsp  39255  rmydioph  39604  expdioph  39613  dmafv2rnb  43421