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  4234  fvopab6  7017  fressnfv  7153  tpostpos  8242  odi  8566  nnmword  8621  ltmpi  10946  maducoeval2  22902  mdbr2  32817  mdsl2i  32843  poimirlem26  38478  poimirlem27  38479  itg2addnclem  38503  itg2addnclem3  38505  xpv  39108  prjspeclsp  43556  rmydioph  43953  expdioph  43962  dmafv2rnb  48215  rexrals  50821  rexals  50827