Theorem iba 536

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ibar  537  biantru  538  biantrud  540  ancrb  556  pm5.54  1033  dedlem0a  1057  r19.29r  3135  unineq  4247  fvopab6  7025  fressnfv  7158  tpostpos  8242  odi  8564  nnmword  8619  ltmpi  10889  maducoeval2  22766  mdbr2  32589  mdsl2i  32615  poimirlem26  38220  poimirlem27  38221  itg2addnclem  38245  itg2addnclem3  38247  xpv  38836  prjspeclsp  43271  rmydioph  43668  expdioph  43677  dmafv2rnb  47890