Theorem iba 537

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 477	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))
2		simpl 488	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜓)
3	1, 2	impbid1 228	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ibar  538  biantru  539  biantrud  541  ancrb  557  pm5.54  1035  dedlem0a  1059  r19.29r  3126  unineq  4233  fvopab6  7028  fressnfv  7164  tpostpos  8263  odi  8587  nnmword  8642  ltmpi  10989  maducoeval2  22955  mdbr2  32898  mdsl2i  32924  poimirlem26  38565  poimirlem27  38566  itg2addnclem  38590  itg2addnclem3  38592  xpv  39195  prjspeclsp  43641  rmydioph  44021  expdioph  44030  dmafv2rnb  48299  rexrals  50905  rexals  50911