Theorem iba 533

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 473	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))
2		simpl 484	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜓)
3	1, 2	impbid1 227	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397

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 209  df-an 398

This theorem is referenced by:  ibar  534  biantru  535  biantrud  537  ancrb  553  pm5.54  1026  dedlem0a  1050  r19.29r  3105  unineq  4219  fvopab6  6974  fressnfv  7107  tpostpos  8190  odi  8508  nnmword  8563  ltmpi  10822  maducoeval2  22627  mdbr2  32389  mdsl2i  32415  poimirlem26  38028  poimirlem27  38029  itg2addnclem  38053  itg2addnclem3  38055  xpv  38644  prjspeclsp  43077  rmydioph  43474  expdioph  43483  dmafv2rnb  47706