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 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400

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 401

This theorem is used by:  ibar  537  biantru  538  biantrud  540  ancrb  556  pm5.54  1034  dedlem0a  1058  r19.29r  3128  unineq  4240  fvopab6  7024  fressnfv  7157  tpostpos  8240  odi  8562  nnmword  8617  ltmpi  10895  maducoeval2  22808  mdbr2  32659  mdsl2i  32685  poimirlem26  38325  poimirlem27  38326  itg2addnclem  38350  itg2addnclem3  38352  xpv  38939  prjspeclsp  43372  rmydioph  43769  expdioph  43778  dmafv2rnb  47994  rexrals  50615  rexals  50621