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  3099  unineq  4239  fvopab6  6975  fressnfv  7105  tpostpos  8188  odi  8506  nnmword  8561  ltmpi  10817  maducoeval2  22586  mdbr2  32352  mdsl2i  32378  poimirlem26  37816  poimirlem27  37817  itg2addnclem  37841  itg2addnclem3  37843  xpv  38432  prjspeclsp  42892  rmydioph  43293  expdioph  43302  dmafv2rnb  47512