Theorem iba 489

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 435	. 2 ⊢ (φ → (ψ → (ψ ∧ φ)))
2		simpl 443	. 2 ⊢ ((ψ ∧ φ) → ψ)
3	1, 2	impbid1 194	1 ⊢ (φ → (ψ ↔ (ψ ∧ φ)))

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358

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 177  df-an 360

This theorem is referenced by:  biantru  491  biantrud  493  ancrb  533  pm5.54  870  rbaibd  876  dedlem0a  918  unineq  3506  dfphi2  4570  opres  4979  resieq  4980  cores  5085  fvres  5343  fressnfv  5440  epelcres  6329