Theorem iba 523

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 463	. 2 ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑)))
2		simpl 472	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜓)
3	1, 2	impbid1 215	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  biantru  525  biantrud  527  ancrb  572  pm5.54  963  rbaibr  966  rbaibd  969  dedlem0a  1012  unineq  3910  fvopab6  6350  fressnfv  6467  tpostpos  7417  odi  7704  nnmword  7758  ltmpi  9764  maducoeval2  20494  hausdiag  21496  mdbr2  29283  mdsl2i  29309  poimirlem26  33565  poimirlem27  33566  itg2addnclem  33591  itg2addnclem3  33593  rmydioph  37898  expdioph  37907