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  3128  unineq  4237  fvopab6  7025  fressnfv  7160  tpostpos  8247  odi  8569  nnmword  8624  ltmpi  10916  maducoeval2  22863  mdbr2  32763  mdsl2i  32789  poimirlem26  38382  poimirlem27  38383  itg2addnclem  38407  itg2addnclem3  38409  xpv  38997  prjspeclsp  43445  rmydioph  43842  expdioph  43851  dmafv2rnb  48104  rexrals  50725  rexals  50731