Theorem iba 535

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

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

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 400

This theorem is referenced by:  ibar  536  biantru  537  biantrud  539  ancrb  555  pm5.54  1031  dedlem0a  1055  r19.29r  3128  unineq  4242  fvopab6  7012  fressnfv  7145  tpostpos  8228  odi  8550  nnmword  8605  ltmpi  10864  maducoeval2  22702  mdbr2  32501  mdsl2i  32527  poimirlem26  38150  poimirlem27  38151  itg2addnclem  38175  itg2addnclem3  38177  xpv  38766  prjspeclsp  43199  rmydioph  43596  expdioph  43605  dmafv2rnb  47828