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  3130  unineq  4236  fvopab6  7048  fressnfv  7185  tpostpos  8288  odi  8612  nnmword  8667  ltmpi  11013  maducoeval2  22982  mdbr2  32925  mdsl2i  32951  poimirlem26  38755  poimirlem27  38756  itg2addnclem  38780  itg2addnclem3  38782  xpv  39385  prjspeclsp  43831  rmydioph  44212  expdioph  44221  dmafv2rnb  48502  rexrals  51183  rexals  51189